GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-11-25 07:13:59 +03:00
Code Issues Projects Releases Wiki Activity

Draft: BaseVariantType

Browse Source 
TODO RGS: Cite T251

[ci skip]
This commit is contained in:
Ryan Scott 2024-01-16 08:53:48 -05:00 committed by Ryan Scott
parent 6f9915b553
commit 80231d4fa1
17 changed files with 482 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
what4/src/What4/BaseTypes.hs
View File

@ -43,6 +43,7 @@ module What4.BaseTypes
, BaseComplexType
, BaseStructType
, BaseArrayType
, BaseVariantType
-- * StringInfo data kind
, StringInfo
-- ** Constructors for StringInfo
@ -138,6 +139,8 @@ data BaseType
-- array in a programming language, but the solver does provide
-- operations for doing pointwise updates.
| BaseArrayType (Ctx.Ctx BaseType) BaseType
-- | TODO RGS: Docs
| BaseVariantType (Ctx.Ctx (Ctx.Ctx BaseType))
type BaseBoolType = 'BaseBoolType -- ^ @:: 'BaseType'@.
type BaseIntegerType = 'BaseIntegerType -- ^ @:: 'BaseType'@.
@ -148,6 +151,7 @@ type BaseStringType = 'BaseStringType -- ^ @:: 'BaseType'@.
type BaseComplexType = 'BaseComplexType -- ^ @:: 'BaseType'@.
type BaseStructType = 'BaseStructType -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'BaseType'@.
type BaseArrayType = 'BaseArrayType -- ^ @:: 'Ctx.Ctx' 'BaseType' -> 'BaseType' -> 'BaseType'@.
type BaseVariantType = 'BaseVariantType -- ^ @:: 'Ctx.Ctx' ('Ctx.Ctx' 'BaseType') -> 'BaseType'@
-- | This data kind describes the types of floating-point formats.
-- This consist of the standard IEEE 754-2008 binary floating point formats.
@ -190,6 +194,10 @@ data BaseTypeRepr (bt::BaseType) :: Type where
-> !(BaseTypeRepr xs)
-> BaseTypeRepr (BaseArrayType (idx Ctx.::> tp) xs)
-- | TODO RGS: Docs
BaseVariantRepr :: !(Ctx.Assignment (Ctx.Assignment BaseTypeRepr) (vs Ctx.::> v))
-> BaseTypeRepr (BaseVariantType (vs Ctx.::> v))
data FloatPrecisionRepr (fpp :: FloatPrecision) where
FloatingPointPrecisionRepr
:: (2 <= eb, 2 <= sb)
@ -253,6 +261,12 @@ instance ( KnownRepr (Ctx.Assignment BaseTypeRepr) idx
=> KnownRepr BaseTypeRepr (BaseArrayType (idx Ctx.::> tp) t) where
knownRepr = BaseArrayRepr knownRepr knownRepr
instance ( KnownRepr (Ctx.Assignment (Ctx.Assignment BaseTypeRepr)) vs
, KnownRepr (Ctx.Assignment BaseTypeRepr) v
)
=> KnownRepr BaseTypeRepr (BaseVariantType (vs Ctx.::> v)) where
knownRepr = BaseVariantRepr knownRepr
instance (2 <= eb, 2 <= es, KnownNat eb, KnownNat es) => KnownRepr FloatPrecisionRepr (FloatingPointPrecision eb es) where
knownRepr = FloatingPointPrecisionRepr knownNat knownNat

9
what4/src/What4/Concrete.hs
View File

@ -83,6 +83,11 @@ data ConcreteVal tp where
ConcreteVal b {- A default value -} ->
Map (Ctx.Assignment ConcreteVal (idx ::> i)) (ConcreteVal b) {- A collection of point-updates -} ->
ConcreteVal (BaseArrayType (idx ::> i) b)
ConcreteVariant ::
Ctx.Assignment (Ctx.Assignment BaseTypeRepr) (vs Ctx.::> v) ->
Ctx.Index (vs Ctx.::> v) flds ->
Ctx.Assignment ConcreteVal flds ->
ConcreteVal (BaseVariantType (vs Ctx.::> v))
deriving instance ShowF ConcreteVal
deriving instance Show (ConcreteVal tp)
@ -117,6 +122,7 @@ concreteType = \case
ConcreteBV w _ -> BaseBVRepr w
ConcreteStruct xs -> BaseStructRepr (fmapFC concreteType xs)
ConcreteArray idxTy def _ -> BaseArrayRepr idxTy (concreteType def)
ConcreteVariant btys _ _ -> BaseVariantRepr btys
$(return [])
@ -124,6 +130,7 @@ instance TestEquality ConcreteVal where
testEquality = $(structuralTypeEquality [t|ConcreteVal|]
[ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|Ctx.Assignment|] `TypeApp` AnyType `TypeApp` AnyType, [|testEqualityFC testEquality|])
, (ConType [t|Ctx.Index|] `TypeApp` AnyType `TypeApp` AnyType, [|testEquality|])
, (ConType [t|ConcreteVal|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|StringLiteral|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|FloatPrecisionRepr|] `TypeApp` AnyType, [|testEquality|])
@ -137,6 +144,7 @@ instance OrdF ConcreteVal where
compareF = $(structuralTypeOrd [t|ConcreteVal|]
[ (ConType [t|NatRepr|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|Ctx.Assignment|] `TypeApp` AnyType `TypeApp` AnyType, [|compareFC compareF|])
, (ConType [t|Ctx.Index|] `TypeApp` AnyType `TypeApp` AnyType, [|compareF|])
, (ConType [t|ConcreteVal|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|StringLiteral|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|FloatPrecisionRepr|] `TypeApp` AnyType, [|compareF|])
@ -173,3 +181,4 @@ ppConcrete = \case
PP.<> PP.comma
PP.<> doc
PP.<> PP.pretty ")"
ConcreteVariant _ _ _ -> PP.pretty "TODO RGS"

65
what4/src/What4/Expr/App.hs
View File

@ -58,6 +58,7 @@ import Data.Parameterized.Nonce
import Data.Parameterized.Some
import Data.Parameterized.TH.GADT
import Data.Parameterized.TraversableFC
import Data.Parameterized.TraversableFC.WithIndex
import Data.Ratio (numerator, denominator)
import qualified Data.Sequence as Seq
import Data.Set (Set)
@ -642,6 +643,33 @@ data App (e :: BaseType -> Type) (tp :: BaseType) where
-> !(BaseTypeRepr tp)
-> App e tp
------------------------------------------------------------------------
-- Variants
-- A variant with its fields.
VariantCtor :: !(Ctx.Assignment (Ctx.Assignment BaseTypeRepr) (vs Ctx.::> v))
-> !(Ctx.Index (vs Ctx.::> v) flds)
-> !(Ctx.Assignment e flds)
-> App e (BaseVariantType (vs Ctx.::> v))
VariantField :: !(e (BaseVariantType vs))
-> !(Ctx.Index vs v)
-> !(Ctx.Index v fld)
-> !(BaseTypeRepr fld)
-> App e fld
VariantTest :: !(e (BaseVariantType vs))
-> !(Ctx.Index vs v)
-> App e BaseBoolType
{-
-- TODO RGS
VariantMatch :: !(e (BaseVariantType vs))
-> !(BaseTypeRepr tp)
-> !(forall v. Ctx.Index vs v -> Ctx.Assignment e v -> App e tp)
-> App e tp
-}
-- | The Kind of a bound variable.
data VarKind
= QuantifierVarKind
@ -796,6 +824,9 @@ traverseApp =
, ( ConType [t|Ctx.Assignment BaseTypeRepr|] `TypeApp` AnyType
, [|(\_ -> pure) |]
)
, ( ConType [t|Ctx.Assignment (Ctx.Assignment BaseTypeRepr)|] `TypeApp` AnyType
, [|(\_ -> pure) |]
)
, ( ConType [t|WeightedSum|] `TypeApp` AnyType `TypeApp` AnyType
, [| WSum.traverseVars |]
)
@ -1897,6 +1928,9 @@ appType a =
StructCtor flds _ -> BaseStructRepr flds
StructField _ _ tp -> tp
VariantCtor vs _ _ -> BaseVariantRepr vs
VariantField _ _ _ tp -> tp
VariantTest{} -> knownRepr
------------------------------------------------------------------------
-- abstractEval
@ -2074,6 +2108,23 @@ abstractEval f a0 = do
StructCtor _ flds -> fmapFC (\v -> AbstractValueWrapper (f v)) flds
StructField s idx _ -> unwrapAV (f s Ctx.! idx)
VariantCtor variantFldTyss idx flds ->
imapFC
(\idx' variantFldTys ->
case testEquality idx idx' of
Just Refl ->
fmapFC
(\fld ->
AbstractValueWrapper (f fld))
flds
_ ->
Ctx.generate
(Ctx.size variantFldTys)
(\idx'' ->
AbstractValueWrapper (avTop (variantFldTys Ctx.! idx''))))
variantFldTyss
VariantField v vIdx fldIdx _ -> unwrapAV ((f v Ctx.! vIdx) Ctx.! fldIdx)
VariantTest{} -> Nothing
reduceApp :: IsExprBuilder sym
=> sym
@ -2237,6 +2288,11 @@ reduceApp sym unary a0 = do
StructCtor _ args -> mkStruct sym args
StructField s i _ -> structField sym s i
VariantCtor vs idx flds -> mkVariant sym vs idx flds
VariantField vs vIdx fldIdx _ -> variantField sym vs vIdx fldIdx
VariantTest v idx -> variantTest sym v idx
-- VariantMatch v f -> variantMatch sym v f
------------------------------------------------------------------------
-- App operations
@ -2270,6 +2326,7 @@ ppVarTypeCode tp =
BaseComplexRepr -> "c"
BaseArrayRepr _ _ -> "a"
BaseStructRepr _ -> "struct"
BaseVariantRepr _ -> "variant"
-- | Either a argument or text or text
data PrettyArg (e :: BaseType -> Type) where
@ -2556,3 +2613,11 @@ ppApp' a0 = do
StructCtor _ flds -> prettyApp "struct" (toListFC exprPrettyArg flds)
StructField s idx _ ->
prettyApp "field" [exprPrettyArg s, showPrettyArg idx]
------------------------------------------------------------------------
-- SymVariant
VariantCtor _ _ _ -> error "TODO RGS"
VariantField _ _ _ _ -> error "TODO RGS"
VariantTest _ _ -> error "TODO RGS"
-- VariantMatch _ _ -> error "TODO RGS"

11
what4/src/What4/Expr/AppTheory.hs
View File

@ -36,6 +36,8 @@ data AppTheory
-- ^ Theory attributed to structs (equivalent to records in CVC4/CVC5/Z3, tuples in Yices)
| FnTheory
-- ^ Theory attributed application functions.
| VariantTheory
-- ^ Theory attributed to variants (equivalent to datatypes in CVC4/CVC5/Z3)
deriving (Eq, Ord)
quantTheory :: NonceApp t (Expr t) tp -> AppTheory
@ -60,6 +62,7 @@ typeTheory tp = case tp of
BaseComplexRepr -> LinearArithTheory
BaseStructRepr _ -> StructTheory
BaseArrayRepr _ _ -> ArrayTheory
BaseVariantRepr _ -> VariantTheory
appTheory :: App (Expr t) tp -> AppTheory
appTheory a0 =
@ -223,3 +226,11 @@ appTheory a0 =
-- A struct with its fields.
StructCtor{} -> StructTheory
StructField{} -> StructTheory
---------------------
-- Variant operations
VariantCtor{} -> VariantTheory
VariantField{} -> VariantTheory
VariantTest{} -> VariantTheory
-- VariantMatch{} -> VariantTheory

43
what4/src/What4/Expr/Builder.hs
View File

@ -2751,6 +2751,9 @@ instance IsExprBuilder (ExprBuilder t st fs) where
| otherwise = sbMakeExpr sym $ BVCountLeadingZeros w x
where w = bvWidth x
----------------------------------------------------------------------
-- Struct operations
mkStruct sym args = do
sbMakeExpr sym $ StructCtor (fmapFC exprType args) args
@ -2767,6 +2770,46 @@ instance IsExprBuilder (ExprBuilder t st fs) where
| x == y = return x
| otherwise = mkIte sym p x y
----------------------------------------------------------------------
-- Variant operations
mkVariant sym vs idx flds =
sbMakeExpr sym $ VariantCtor vs idx flds
variantField sym v vIdx fldIdx
| Just (VariantCtor _ vIdx' flds) <- asApp v
, Just Refl <- testEquality vIdx vIdx'
= return $! flds Ctx.! fldIdx
| otherwise = do
case exprType v of
BaseVariantRepr vs ->
sbMakeExpr sym $
VariantField v vIdx fldIdx ((vs Ctx.! vIdx) Ctx.! fldIdx)
variantTest sym v idx
| Just (VariantCtor _ idx' _) <- asApp v
= case testEquality idx idx' of
Just Refl -> return $! truePred sym
Nothing -> return $! falsePred sym
| otherwise
= sbMakeExpr sym $ VariantTest v idx
{-
variantMatch sym v f
| Just (VariantCtor _ idx flds) <- asApp v
= f idx flds
{-
| otherwise
= -- TODO RGS
-}
-}
variantIte sym p x y
| Just True <- asConstantPred p = return x
| Just False <- asConstantPred p = return y
| x == y = return x
| otherwise = mkIte sym p x y
--------------------------------------------------------------------
-- String operations

36
what4/src/What4/Expr/GroundEval.hs
View File

@ -46,9 +46,10 @@ import qualified Data.BitVector.Sized as BV
import Data.List.NonEmpty (NonEmpty(..))
import Data.Foldable
import qualified Data.Map.Strict as Map
import Data.Maybe ( fromMaybe )
import Data.Maybe ( fromMaybe, isJust )
import Data.Parameterized.Ctx
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Pair (Pair(..))
import Data.Parameterized.NatRepr
import Data.Parameterized.TraversableFC
import Data.Ratio
@ -82,6 +83,7 @@ type family GroundValue (tp :: BaseType) where
GroundValue (BaseStringType si) = StringLiteral si
GroundValue (BaseArrayType idx b) = GroundArray idx b
GroundValue (BaseStructType ctx) = Ctx.Assignment GroundValueWrapper ctx
GroundValue (BaseVariantType ctx) = Pair (Ctx.Index ctx) (Ctx.Assignment GroundValueWrapper)
-- | A function that calculates ground values for elements.
-- Clients of solvers should use the @groundEval@ function for computing
@ -165,6 +167,10 @@ defaultValueForType tp =
BaseArrayRepr _ b -> ArrayConcrete (defaultValueForType b) Map.empty
BaseStructRepr ctx -> fmapFC (GVW . defaultValueForType) ctx
BaseFloatRepr _fpp -> BF.bfPosZero
-- TODO RGS: This deserves some commentary
BaseVariantRepr ctx ->
let idx = Ctx.lastIndex (Ctx.size ctx) in
Pair idx (fmapFC (GVW . defaultValueForType) (ctx Ctx.! idx))
{-# INLINABLE evalGroundExpr #-}
-- | Helper function for evaluating @Expr@ expressions in a model.
@ -264,6 +270,17 @@ groundEq bt0 x0 y0 = unMAnd (f bt0 x0 y0)
coerceMAnd (Ctx.traverseWithIndex
(\i tp -> f tp (unGVW (x Ctx.! i)) (unGVW (y Ctx.! i))) flds)
BaseArrayRepr{} -> MAnd Nothing
BaseVariantRepr vs
| Pair xIdx xFlds <- x
, Pair yIdx yFlds <- y
-> case testEquality xIdx yIdx of
Just Refl ->
coerceMAnd $
Ctx.traverseWithIndex
(\i tp -> f tp (unGVW (xFlds Ctx.! i)) (unGVW (yFlds Ctx.! i)))
(vs Ctx.! xIdx)
Nothing ->
MAnd Nothing
-- | Helper function for evaluating @App@ expressions.
--
@ -615,3 +632,20 @@ evalGroundApp f a0 = do
StructField s i _ -> do
sv <- f s
return $! unGVW (sv Ctx.! i)
------------------------------------------------------------------------
-- Variants
VariantCtor _ idx vs -> do
vs' <- traverseFC (\v -> GVW <$> f v) vs
return $! Pair idx vs'
VariantField v vIdx fldIdx _ -> do
Pair vIdx' flds <- f v
case testEquality vIdx vIdx' of
Just Refl ->
return $! unGVW (flds Ctx.! fldIdx)
Nothing ->
mzero
VariantTest v idx -> do
Pair idx' _ <- f v
return $! isJust (testEquality idx idx')

20
what4/src/What4/Expr/VarIdentification.hs
View File

@ -161,15 +161,16 @@ addFeatures f = VR $ problemFeatures %= (.|. f)
addFeaturesForVarType :: BaseTypeRepr tp -> VarRecorder s t ()
addFeaturesForVarType tp =
case tp of
BaseBoolRepr -> return ()
BaseBVRepr _ -> addFeatures useBitvectors
BaseIntegerRepr -> addFeatures useIntegerArithmetic
BaseRealRepr -> addFeatures useLinearArithmetic
BaseComplexRepr -> addFeatures useLinearArithmetic
BaseStringRepr _ -> addFeatures useStrings
BaseArrayRepr{} -> addFeatures useSymbolicArrays
BaseStructRepr{} -> addFeatures useStructs
BaseFloatRepr _ -> addFeatures useFloatingPoint
BaseBoolRepr -> return ()
BaseBVRepr _ -> addFeatures useBitvectors
BaseIntegerRepr -> addFeatures useIntegerArithmetic
BaseRealRepr -> addFeatures useLinearArithmetic
BaseComplexRepr -> addFeatures useLinearArithmetic
BaseStringRepr _ -> addFeatures useStrings
BaseArrayRepr{} -> addFeatures useSymbolicArrays
BaseStructRepr{} -> addFeatures useStructs
BaseFloatRepr _ -> addFeatures useFloatingPoint
BaseVariantRepr{} -> addFeatures useVariants
-- | Information about bound variables outside this context.
@ -407,6 +408,7 @@ addTheoryFeatures th =
StructTheory -> addFeatures useStructs
StringTheory -> addFeatures useStrings
FloatingPointTheory -> addFeatures useFloatingPoint
VariantTheory -> addFeatures useVariants
QuantifierTheory -> return ()
FnTheory -> return ()

149
what4/src/What4/Interface.hs
View File

@ -113,6 +113,7 @@ module What4.Interface
, SymStruct
, SymBV
, SymArray
, SymVariant
-- * Natural numbers
, SymNat
@ -210,7 +211,7 @@ import Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Ctx
import Data.Parameterized.Utils.Endian (Endian(..))
import Data.Parameterized.Map (MapF)
import Data.Parameterized.Map (MapF, Pair(..))
import Data.Parameterized.NatRepr
import Data.Parameterized.TraversableFC
import qualified Data.Parameterized.Vector as Vector
@ -267,6 +268,9 @@ type SymBV sym n = SymExpr sym (BaseBVType n)
-- | Symbolic strings.
type SymString sym si = SymExpr sym (BaseStringType si)
-- | Symbolic variants.
type SymVariant sym vs = SymExpr sym (BaseVariantType vs)
------------------------------------------------------------------------
-- Type families for the interface.
@ -370,6 +374,10 @@ class HasAbsValue e => IsExpr e where
asStruct :: e (BaseStructType flds) -> Maybe (Ctx.Assignment e flds)
asStruct _ = Nothing
-- | TODO RGS: Docs
asVariant :: e (BaseVariantType vs) -> Maybe (Pair (Ctx.Index vs) (Ctx.Assignment e))
asVariant _ = Nothing
-- | Get type of expression.
exprType :: e tp -> BaseTypeRepr tp
@ -635,24 +643,25 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
-- | Return true if two expressions are equal. The default
-- implementation dispatches 'eqPred', 'bvEq', 'natEq', 'intEq',
-- 'realEq', 'cplxEq', 'structEq', or 'arrayEq', depending on the
-- 'realEq', 'cplxEq', 'structEq', 'arrayEq', or 'variantEq' depending on the
-- type.
isEq :: sym -> SymExpr sym tp -> SymExpr sym tp -> IO (Pred sym)
isEq sym x y =
case exprType x of
BaseBoolRepr -> eqPred sym x y
BaseBVRepr{} -> bvEq sym x y
BaseIntegerRepr -> intEq sym x y
BaseRealRepr -> realEq sym x y
BaseFloatRepr{} -> floatEq sym x y
BaseComplexRepr -> cplxEq sym x y
BaseStringRepr{} -> stringEq sym x y
BaseStructRepr{} -> structEq sym x y
BaseArrayRepr{} -> arrayEq sym x y
BaseBoolRepr -> eqPred sym x y
BaseBVRepr{} -> bvEq sym x y
BaseIntegerRepr -> intEq sym x y
BaseRealRepr -> realEq sym x y
BaseFloatRepr{} -> floatEq sym x y
BaseComplexRepr -> cplxEq sym x y
BaseStringRepr{} -> stringEq sym x y
BaseStructRepr{} -> structEq sym x y
BaseArrayRepr{} -> arrayEq sym x y
BaseVariantRepr{} -> variantEq sym x y
-- | Take the if-then-else of two expressions. The default
-- implementation dispatches 'itePred', 'bvIte', 'natIte', 'intIte',
-- 'realIte', 'cplxIte', 'structIte', or 'arrayIte', depending on
-- 'realIte', 'cplxIte', 'structIte', 'arrayIte', or 'variantIte' depending on
-- the type.
baseTypeIte :: sym
-> Pred sym
@ -661,15 +670,16 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
-> IO (SymExpr sym tp)
baseTypeIte sym c x y =
case exprType x of
BaseBoolRepr -> itePred sym c x y
BaseBVRepr{} -> bvIte sym c x y
BaseIntegerRepr -> intIte sym c x y
BaseRealRepr -> realIte sym c x y
BaseFloatRepr{} -> floatIte sym c x y
BaseStringRepr{} -> stringIte sym c x y
BaseComplexRepr -> cplxIte sym c x y
BaseStructRepr{} -> structIte sym c x y
BaseArrayRepr{} -> arrayIte sym c x y
BaseBoolRepr -> itePred sym c x y
BaseBVRepr{} -> bvIte sym c x y
BaseIntegerRepr -> intIte sym c x y
BaseRealRepr -> realIte sym c x y
BaseFloatRepr{} -> floatIte sym c x y
BaseStringRepr{} -> stringIte sym c x y
BaseComplexRepr -> cplxIte sym c x y
BaseStructRepr{} -> structIte sym c x y
BaseArrayRepr{} -> arrayIte sym c x y
BaseVariantRepr{} -> variantIte sym c x y
-- | Given a symbolic expression, annotate it with a unique identifier
-- that can be used to maintain a connection with the given term.
@ -1413,6 +1423,85 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
-> SymStruct sym flds
-> IO (SymStruct sym flds)
----------------------------------------------------------------------
-- Variant operations
-- | Create a variant from the variant index and an assignment of
-- expressions. (TODO RGS: What about the type assignment? Mention it.)
mkVariant :: sym
-> Ctx.Assignment (Ctx.Assignment BaseTypeRepr) (vs Ctx.::> v)
-> Ctx.Index (vs Ctx.::> v) flds
-> Ctx.Assignment (SymExpr sym) flds
-> IO (SymVariant sym (vs Ctx.::> v))
-- | Get the value of a specific field in a variant. The result is undefined
-- if the field does not belong to a variant that is active. (TODO RGS:
-- is `active` the right term?)
variantField :: sym
-> SymVariant sym vs
-> Ctx.Index vs v
-> Ctx.Index v fld
-> IO (SymExpr sym fld)
-- | TODO RGS: Docs
variantTest :: sym
-> SymVariant sym vs
-> Ctx.Index vs v
-> IO (Pred sym)
{-
-- | TODO RGS: Docs
variantMatch :: sym
-> SymVariant sym vs
-> BaseTypeRepr tp
-> (forall v
. Ctx.Index vs v
-> Ctx.Assignment (SymExpr sym) v
-> IO (SymExpr sym tp))
-> IO (SymExpr sym tp)
-}
-- | Check if two variants are equal.
variantEq :: forall vs
. sym
-> SymVariant sym vs
-> SymVariant sym vs
-> IO (Pred sym)
variantEq sym x y =
case exprType x of
BaseVariantRepr vs -> do
let f :: IO (Pred sym)
-> Ctx.Index vs v
-> IO (Pred sym)
f mp vIdx = do
xTest <- variantTest sym x vIdx
yTest <- variantTest sym y vIdx
xyTest <- andPred sym xTest yTest
fldsEq <- Ctx.forIndex (Ctx.size (vs Ctx.! vIdx)) (g vIdx) mp
impliesPred sym xyTest fldsEq
g :: Ctx.Index vs v
-> IO (Pred sym)
-> Ctx.Index v flds
-> IO (Pred sym)
g vIdx mp fldIdx = do
xFld <- variantField sym x vIdx fldIdx
yFld <- variantField sym x vIdx fldIdx
fldEq <- isEq sym xFld yFld
case asConstantPred fldEq of
Just True -> mp
Just False -> return (falsePred sym)
_ -> andPred sym fldEq =<< mp
Ctx.forIndex (Ctx.size vs) f (return (truePred sym))
-- | Take the if-then-else of two variants.
variantIte :: sym
-> Pred sym
-> SymVariant sym flds
-> SymVariant sym flds
-> IO (SymVariant sym flds)
-----------------------------------------------------------------------
-- Array operations
@ -2990,6 +3079,9 @@ baseIsConcrete x =
case asConstantArray x of
Just x' -> baseIsConcrete x'
Nothing -> False
BaseVariantRepr _ -> case asVariant x of
Just (Pair _idx x') -> allFC baseIsConcrete x'
Nothing -> False
-- | Return some default value for each base type.
-- For numeric types, this is 0; for booleans, false;
@ -3017,6 +3109,15 @@ baseDefaultValue sym bt =
BaseArrayRepr idx bt' -> do
elt <- baseDefaultValue sym bt'
constantArray sym idx elt
-- TODO RGS: This deserves some commentary
BaseVariantRepr vs -> do
let f :: BaseTypeRepr tp -> IO (SymExpr sym tp)
f v = baseDefaultValue sym v
idx = Ctx.lastIndex $ Ctx.size vs
flds = vs Ctx.! idx
flds' <- traverseFC f flds
mkVariant sym vs (Ctx.lastIndex (Ctx.size vs)) flds'
-- | Return predicate equivalent to a Boolean.
backendPred :: IsExprBuilder sym => sym -> Bool -> Pred sym
@ -3190,6 +3291,10 @@ asConcrete x =
-- TODO: what about cases where there are updates to the array?
-- Passing Map.empty is probably wrong.
pure (ConcreteArray idx c_def Map.empty)
BaseVariantRepr variants ->
do Pair idx vals <- asVariant x
vals' <- traverseFC asConcrete vals
pure $ ConcreteVariant variants idx vals'
-- | Create a literal symbolic value from a concrete value.
concreteToSym :: IsExprBuilder sym => sym -> ConcreteVal tp -> IO (SymExpr sym tp)
@ -3211,6 +3316,8 @@ concreteToSym sym = \case
i' <- traverseFC (concreteToSym sym) i
x' <- concreteToSym sym x
arrayUpdate sym arr' i' x'
ConcreteVariant variantFldTys idx variantFlds ->
mkVariant sym variantFldTys idx =<< traverseFC (concreteToSym sym) variantFlds
------------------------------------------------------------------------
-- muxNatRange

9
what4/src/What4/ProblemFeatures.hs
View File

@ -46,6 +46,7 @@ module What4.ProblemFeatures
, useUninterpFunctions
, useDefinedFunctions
, useProduceAbducts
, useVariants
, hasProblemFeature
) where
@ -131,11 +132,17 @@ useUninterpFunctions = ProblemFeatures 0x2000
useDefinedFunctions :: ProblemFeatures
useDefinedFunctions = ProblemFeatures 0x4000
-- | Indicates if the solver is able and configured to
-- | Indicates if the solver is able and configured to
-- produce abducts.
useProduceAbducts :: ProblemFeatures
useProduceAbducts = ProblemFeatures 0x8000
-- | Indicates whether the problem uses variants.
--
-- Variants are modeled using datatypes in CVC4/CVC5/Z3.
useVariants :: ProblemFeatures
useVariants = ProblemFeatures 0x10000
-- | Tests if one set of problem features subsumes another.
-- In particular, @hasProblemFeature x y@ is true iff
-- the set of features in @x@ is a superset of those in @y@.

12
what4/src/What4/Protocol/SMTLib2.hs
View File

@ -438,6 +438,18 @@ class Show a => SMTLib2Tweaks a where
]
in SMT2.Cmd $ app "declare-datatype" [ tp, app "par" [ builder_list tp_names, builder_list [app cnstr flds]]]
{-
-- TODO RGS: Docs
-- | The sort of variants with the given field types.
--
-- By default, this uses SMTLIB2 datatypes and are not primitive to the language.
smtlib2VariantSort :: NonEmpty [SMT2.Sort] -> SMT2.Sort
smtlib2VariantSort flds = SMT2.Sort $ "(Struct" <> Builder.decimal n <> foldMap f flds <> ")"
where f :: SMT2.Sort -> Builder
f (SMT2.Sort s) = " " <> s
n = length flds
-}
asSMT2Type :: forall a tp . SMTLib2Tweaks a => TypeMap tp -> SMT2.Sort

81
what4/src/What4/Protocol/SMTWriter.hs
View File

@ -210,6 +210,11 @@ data TypeMap (tp::BaseType) where
StructTypeMap :: !(Ctx.Assignment TypeMap idx)
-> TypeMap (BaseStructType idx)
-- A variant encoded as an SMTLIB datatype.
--
-- None of the fields should be arrays encoded as functions.
VariantTypeMap :: !(Ctx.Assignment (Ctx.Assignment TypeMap) idx)
-> TypeMap (BaseVariantType idx)
instance ShowF TypeMap
@ -225,6 +230,7 @@ instance Show (TypeMap a) where
show (PrimArrayTypeMap ctx a) = "PrimArrayTypeMap " ++ showF ctx ++ " " ++ showF a
show (FnArrayTypeMap ctx a) = "FnArrayTypeMap " ++ showF ctx ++ " " ++ showF a
show (StructTypeMap ctx) = "StructTypeMap " ++ showF ctx
show (VariantTypeMap ctx) = "VariantTypeMap " ++ showF ctx
instance Eq (TypeMap tp) where
@ -970,12 +976,34 @@ class (SupportTermOps (Term h)) => SMTWriter h where
-- arguments in the struct.
declareStructDatatype :: WriterConn t h -> Ctx.Assignment TypeMap args -> IO ()
-- | Declare a variant datatype (if is has not been already) given the number
-- of variants and field types.
declareVariantDatatype :: WriterConn t h
-> Ctx.Assignment (Ctx.Assignment TypeMap) args
-> IO ()
-- | Build a struct term with the given types and fields
structCtor :: Ctx.Assignment TypeMap args -> [Term h] -> Term h
-- | Project a field from a struct with the given types
structProj :: Ctx.Assignment TypeMap args -> Ctx.Index args tp -> Term h -> Term h
-- | Build a struct term with the given types and fields
variantCtor :: Ctx.Assignment (Ctx.Assignment TypeMap) vs
-> Ctx.Index vs v
-> [Term h]
-> Term h
-- | Project a field from a struct with the given types
variantProj :: Ctx.Assignment (Ctx.Assignment TypeMap) vs
-> Ctx.Index vs v
-> Ctx.Index v fld
-> Term h
-> Term h
-- | TODO RGS: Docs
variantTest :: Ctx.Index vs v -> Term h -> Term h
-- | Produce a term representing a string literal
stringTerm :: Text -> Term h
@ -1172,6 +1200,9 @@ declareTypes conn = \case
StructTypeMap flds ->
do traverseFC_ (declareTypes conn) flds
declareStructDatatype conn flds
VariantTypeMap vs ->
do traverseFC_ (traverseFC_ (declareTypes conn)) vs
declareVariantDatatype conn vs
data DefineStyle
@ -1300,6 +1331,8 @@ typeMapFirstClass conn tp0 = do
<*> typeMapFirstClass conn eltTp
BaseStructRepr flds ->
StructTypeMap <$> traverseFC (typeMapFirstClass conn) flds
BaseVariantRepr vs ->
VariantTypeMap <$> traverseFC (traverseFC (typeMapFirstClass conn)) vs
getBaseSMT_Type :: ExprBoundVar t tp -> SMTCollector t h (TypeMap tp)
getBaseSMT_Type v = do
@ -1441,6 +1474,26 @@ addPartialSideCond conn t (StructTypeMap ctx) (Just abvs) =
(Just (unwrapAV (abvs Ctx.! i))))
(return ())
addPartialSideCond conn t (VariantTypeMap ctx) (Just abvs) =
error "TODO RGS"
{-
-- TODO RGS: Docs
addPartialSideCond conn t (VariantTypeMap ctx) (Just abvs) =
Ctx.forIndex
(Ctx.size ctx)
(\start i ->
Ctx.forIndex
(Ctx.size (ctx Ctx.! i))
(\start' j ->
do start'
addPartialSideCond conn
(structProj @h ctx i t)
(ctx Ctx.! i)
(Just (unwrapAV (abvs Ctx.! i))))
start)
(return ())
-}
addPartialSideCond _ _t (PrimArrayTypeMap _idxTp _resTp) (Just _abv) =
fail "SMTWriter.addPartialSideCond: bounds on array values not supported"
addPartialSideCond _ _t (FnArrayTypeMap _idxTp _resTp) (Just _abv) =
@ -2918,6 +2971,32 @@ appSMTExpr ae = do
let tm = structProj @h flds idx (asBase expr)
freshBoundTerm tp tm
--------------------------------------------------------------------
-- Variants
VariantCtor vs idx flds -> do
-- Make sure a variant datatype with these fields has been declared.
exprs <- traverseFC mkExpr flds
vs_types <-
traverseFC (traverseFC (evalFirstClassTypeRepr conn (eltSource i))) vs
liftIO $ declareVariantDatatype conn vs_types
let tm = variantCtor @h vs_types idx (toListFC asBase exprs)
freshBoundTerm (VariantTypeMap vs_types) tm
VariantField v vIdx fldIdx _tp -> do
expr <- mkExpr v
case smtExprType expr of
VariantTypeMap flds -> do
let tp = (flds Ctx.! vIdx) Ctx.! fldIdx
let tm = variantProj @h flds vIdx fldIdx (asBase expr)
freshBoundTerm tp tm
VariantTest v idx -> do
expr <- mkExpr v
let tm = variantTest @h idx (asBase expr)
freshBoundTerm BoolTypeMap tm
defineFn :: SMTWriter h
=> WriterConn t h
-> Text
@ -3157,6 +3236,8 @@ getSolverVal conn smtFns (StructTypeMap flds0) tm =
-> IO (GroundValueWrapper utp)
f flds i tp = GVW <$> getSolverVal conn smtFns tp v
where v = structProj @h flds i tm
getSolverVal conn smtFns (VariantTypeMap vs0) tm =
error "TODO RGS"
-- | The function creates a function for evaluating elts to concrete values
-- given a connection to an SMT solver along with some functions for evaluating

6
what4/src/What4/Protocol/VerilogWriter/Backend.hs
View File

@ -357,6 +357,12 @@ appVerilogExpr app =
StructCtor _ _ -> doNotSupportError "structs"
StructField _ _ _ -> doNotSupportError "structs"
-- Variants
VariantCtor _ _ _ -> doNotSupportError "variants"
VariantField _ _ _ _ -> doNotSupportError "variants"
VariantTest _ _ -> doNotSupportError "variants"
-- VariantMatch _ _ _ -> doNotSupportError "variants"
-- Strings
StringAppend _ _ -> doNotSupportError "strings"
StringContains _ _ -> doNotSupportError "strings"

2
what4/src/What4/Serialize/Printer.hs
View File

@ -370,6 +370,7 @@ freshName tp = do
W4.BaseBVRepr{} -> "bv"
W4.BaseStructRepr{} -> "struct"
W4.BaseArrayRepr{} -> "arr"
W4.BaseVariantRepr{} -> "variant"
return $ T.pack $ prefix++(show $ idCount)
freshFnName :: W4.ExprSymFn t args ret -> Memo t Text
@ -762,6 +763,7 @@ convertBaseType tp = case tp of
W4.BaseArrayRepr ixs repr -> S.L [S.A (AId "Array"), S.L $ convertBaseTypes ixs , convertBaseType repr]
W4.BaseFloatRepr (W4.FloatingPointPrecisionRepr eRepr sRepr) ->
S.L [ S.A (AId "Float"), S.A (AInt (NR.intValue eRepr)), S.A (AInt (NR.intValue sRepr)) ]
W4.BaseVariantRepr _ -> error "TODO RGS"

1
what4/src/What4/Solver/CVC4.hs
View File

@ -148,6 +148,7 @@ cvc4Features = useComputableReals
.|. useFloatingPoint
.|. useBitvectors
.|. useQuantifiers
.|. useVariants
writeMultiAsmpCVC4SMT2File
:: ExprBuilder t st fs

1
what4/src/What4/Solver/CVC5.hs
View File

@ -147,6 +147,7 @@ cvc5Features = useComputableReals
.|. useBitvectors
.|. useQuantifiers
.|. useProduceAbducts
.|. useVariants
writeMultiAsmpCVC5SMT2File
:: ExprBuilder t st fs

1
what4/src/What4/Solver/Z3.hs
View File

@ -158,6 +158,7 @@ z3Features = useNonlinearArithmetic
.|. useStrings
.|. useFloatingPoint
.|. useBitvectors
.|. useVariants
writeZ3SMT2File
:: ExprBuilder t st fs

54
what4/src/What4/Utils/AbstractDomains.hs
View File

@ -104,7 +104,9 @@ import Control.Exception (assert)
import Data.Kind
import Data.Parameterized.Context as Ctx
import Data.Parameterized.NatRepr
import Data.Parameterized.Pair
import Data.Parameterized.TraversableFC
import Data.Parameterized.TraversableFC.WithIndex
import Data.Ratio (denominator)
import What4.BaseTypes
@ -660,6 +662,7 @@ type family AbstractValue (tp::BaseType) :: Type where
AbstractValue BaseComplexType = Complex RealAbstractValue
AbstractValue (BaseArrayType idx b) = AbstractValue b
AbstractValue (BaseStructType ctx) = Ctx.Assignment AbstractValueWrapper ctx
AbstractValue (BaseVariantType ctx) = Ctx.Assignment (Ctx.Assignment AbstractValueWrapper) ctx
-- | A utility class for values that contain abstract values
@ -679,6 +682,7 @@ type family ConcreteValue (tp::BaseType) :: Type where
ConcreteValue BaseComplexType = Complex Rational
ConcreteValue (BaseArrayType idx b) = ()
ConcreteValue (BaseStructType ctx) = Ctx.Assignment ConcreteValueWrapper ctx
ConcreteValue (BaseVariantType ctx) = Pair (Index ctx) (Assignment ConcreteValueWrapper)
newtype ConcreteValueWrapper tp
= ConcreteValueWrapper { unwrapCV :: ConcreteValue tp }
@ -696,6 +700,7 @@ avTop tp =
BaseFloatRepr{} -> ()
BaseArrayRepr _a b -> avTop b
BaseStructRepr flds -> fmapFC (\etp -> AbstractValueWrapper (avTop etp)) flds
BaseVariantRepr vs -> fmapFC (fmapFC (\etp -> AbstractValueWrapper (avTop etp))) vs
-- | Create an abstract value that contains the given concrete value.
avSingle :: BaseTypeRepr tp -> ConcreteValue tp -> AbstractValue tp
@ -714,6 +719,23 @@ avSingle tp =
(\ftp v -> AbstractValueWrapper (avSingle ftp (unwrapCV v)))
flds
vals
BaseVariantRepr variantFldTyss -> \(Pair idx flds) ->
imapFC
(\idx' variantFldTys ->
case testEquality idx idx' of
Just Refl ->
imapFC
(\idx'' fld ->
AbstractValueWrapper
(avSingle
(variantFldTys Ctx.! idx'')
(unwrapCV fld)))
flds
_ ->
Ctx.generate
(Ctx.size variantFldTys)
(\idx'' -> AbstractValueWrapper (avTop (variantFldTys Ctx.! idx''))))
variantFldTyss
------------------------------------------------------------------------
-- Abstractable
@ -814,6 +836,37 @@ instance Abstractable (BaseStructType ctx) where
u = x Ctx.! i
v = y Ctx.! i
instance Abstractable (BaseVariantType ctx) where
avJoin (BaseVariantRepr vs) x y = ctxZipWith3 (ctxZipWith3 avJoin') vs x y
avOverlap (BaseVariantRepr vFldss) xss yss = Ctx.forIndex (Ctx.size vFldss) f False
where f :: forall tp. Bool -> Ctx.Index ctx tp -> Bool
f b1 i = Ctx.forIndex (Ctx.size vFlds) (g vFlds xs ys) b1
where vFlds = vFldss Ctx.! i
xs = xss Ctx.! i
ys = yss Ctx.! i
g ::
forall ctx' tp'.
Assignment BaseTypeRepr ctx' ->
Assignment AbstractValueWrapper ctx' ->
Assignment AbstractValueWrapper ctx' ->
Bool -> Ctx.Index ctx' tp' -> Bool
g vFlds' xs' ys' b2 j =
withAbstractable tp (avOverlap tp (unwrapAV x) (unwrapAV y)) && b2
where tp = vFlds' Ctx.! j
x = xs' Ctx.! j
y = ys' Ctx.! j
avCheckEq = error "TODO RGS"
{-
avCheckEq (BaseVariantRepr vs) x y = Ctx.forIndex (Ctx.size vs) f (Just True)
where f :: Maybe Bool -> Ctx.Index ctx tp -> Maybe Bool
f b i = combineEqCheck b (withAbstractable tp (avCheckEq tp (unwrapAV u) (unwrapAV v)))
where tp = flds Ctx.! i
u = x Ctx.! i
v = y Ctx.! i
-}
withAbstractable
:: BaseTypeRepr bt
-> (Abstractable bt => a)
@ -829,6 +882,7 @@ withAbstractable bt k =
BaseArrayRepr _a _b -> k
BaseStructRepr _flds -> k
BaseFloatRepr _fpp -> k
BaseVariantRepr _vs -> k
-- | Returns true if the concrete value is a member of the set represented
-- by the abstract value.