diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,8 @@ +2024-09-07 + * Version bump (4.0). (#532) + * Add support for struct updates in Copilot.Theorem.What4. (#524) + * Add support for array updates in Copilot.Theorem.What4. (#36) + 2024-07-07 * Version bump (3.20). (#522) * What4 upper-bound dependency version bump. (#514) diff --git a/copilot-theorem.cabal b/copilot-theorem.cabal --- a/copilot-theorem.cabal +++ b/copilot-theorem.cabal @@ -14,7 +14,7 @@ . -version : 3.20 +version : 4.0 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -63,8 +63,8 @@ , xml >= 1.3 && < 1.4 , what4 >= 1.3 && < 1.7 - , copilot-core >= 3.20 && < 3.21 - , copilot-prettyprinter >= 3.20 && < 3.21 + , copilot-core >= 4.0 && < 4.1 + , copilot-prettyprinter >= 4.0 && < 4.1 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove diff --git a/src/Copilot/Theorem/What4/Translate.hs b/src/Copilot/Theorem/What4/Translate.hs --- a/src/Copilot/Theorem/What4/Translate.hs +++ b/src/Copilot/Theorem/What4/Translate.hs @@ -52,16 +52,18 @@ import Data.Parameterized.Classes (KnownRepr (..)) import Data.Parameterized.Context (EmptyCtx, type (::>)) import Data.Parameterized.NatRepr (LeqProof (..), NatCases (..), - NatRepr, decNat, isZeroOrGT1, + NatRepr, decNat, incNat, + intValue, isZeroOrGT1, knownNat, minusPlusCancel, - mkNatRepr, testNatCases) + mkNatRepr, testNatCases, + testStrictLeq) import Data.Parameterized.Some (Some (..)) import Data.Parameterized.SymbolRepr (SymbolRepr, knownSymbol) import qualified Data.Parameterized.Vector as V import Data.Type.Equality (TestEquality (..), (:~:) (..)) import Data.Word (Word32) import GHC.TypeLits (KnownSymbol) -import GHC.TypeNats (KnownNat, type (<=)) +import GHC.TypeNats (KnownNat, type (<=), type (+)) import qualified Panic as Panic import qualified What4.BaseTypes as WT @@ -799,6 +801,8 @@ (CE.BwShiftL _ _, xe1, xe2) -> translateBwShiftL xe1 xe2 (CE.BwShiftR _ _, xe1, xe2) -> translateBwShiftR xe1 xe2 (CE.Index _, xe1, xe2) -> translateIndex xe1 xe2 + (CE.UpdateField atp _ftp extractor, structXe, fieldXe) -> + translateUpdateField atp extractor structXe fieldXe where -- Translate an 'CE.Add' operation and its arguments into a what4 -- representation of the appropriate type. @@ -964,6 +968,55 @@ liftIO $ buildIndexExpr sym ix xes _ -> unexpectedValues "index operation" + -- Translate an 'CE.UpdateField' operation and its arguments into a what4 + -- representation. This function will panic if one of the following does not + -- hold: + -- + -- - The argument is not a struct. + -- + -- - The struct's field cannot be found. + translateUpdateField :: forall struct s. + KnownSymbol s + => CT.Type struct + -- ^ The type of the struct argument + -> (struct -> CT.Field s b) + -- ^ Extract a struct field + -> XExpr sym + -- ^ The first argument value (should be a struct) + -> XExpr sym + -- ^ The second argument value (should be the same type + -- as the struct field) + -> TransM sym (XExpr sym) + -- ^ The first argument value, but with an updated + -- value for the supplied field. + translateUpdateField structTp extractor structXe newFieldXe = + case (structTp, structXe) of + (CT.Struct s, XStruct structFieldXes) -> + case mIx s of + Just ix -> return $ XStruct $ updateAt ix newFieldXe structFieldXes + Nothing -> + panic [ "Could not find field " ++ show fieldNameRepr + , show s + ] + _ -> unexpectedValues "update-field operation" + where + -- Update an element of a list at a particular index. This assumes the + -- preconditions that the index is a non-negative number that is less + -- than the length of the list. + updateAt :: forall a. Int -> a -> [a] -> [a] + updateAt _ _ [] = [] + updateAt 0 new (_:xs) = new : xs + updateAt n new (x:xs) = x : updateAt (n-1) new xs + + fieldNameRepr :: SymbolRepr s + fieldNameRepr = fieldName (extractor undefined) + + structFieldNameReprs :: CT.Struct struct => struct -> [Some SymbolRepr] + structFieldNameReprs s = valueName <$> CT.toValues s + + mIx :: CT.Struct struct => struct -> Maybe Int + mIx s = elemIndex (Some fieldNameRepr) (structFieldNameReprs s) + -- Check the types of the arguments. If the arguments are bitvector values, -- apply the 'BVOp2'. If the arguments are floating-point values, apply the -- 'FPOp2'. Otherwise, 'panic'. @@ -1090,7 +1143,37 @@ translateOp3 sym origExpr op xe1 xe2 xe3 = case (op, xe1, xe2, xe3) of (CE.Mux _, XBool te, xe1, xe2) -> liftIO $ mkIte sym te xe1 xe2 (CE.Mux _, _, _, _) -> unexpectedValues "mux operation" + (CE.UpdateArray _, xe1, xe2, xe3) -> translateUpdateArray xe1 xe2 xe3 where + -- Translate an 'CE.UpdateArray' operation and its arguments into a what4 + -- representation. This checks that the first argument is an 'XArray' and + -- the second argument is an 'XWord32', invoking 'panic' is this invariant + -- is not upheld. + -- + -- Note: Currently, copilot only checks if array indices are out of bounds + -- as a side condition. The method of translation we are using simply + -- creates a nest of if-then-else expression to check the index expression + -- against all possible indices. If the index expression is known by the + -- solver to be out of bounds (for instance, if it is a constant 5 for an + -- array of 5 elements), then the if-then-else will trivially resolve to + -- true. + translateUpdateArray :: XExpr sym + -> XExpr sym + -> XExpr sym + -> TransM sym (XExpr sym) + translateUpdateArray xe1 xe2 newXe = case (xe1, xe2) of + (XArray xes, XWord32 ix) -> do + -- The second argument should not be out of bounds (i.e., greater than + -- or equal to the length of the array) + xesLenBV <- liftIO $ WI.bvLit sym knownNat $ BV.mkBV knownNat + $ toInteger $ V.lengthInt xes + inRange <- liftIO $ WI.bvUlt sym ix xesLenBV + addSidePred inRange + + xes' <- liftIO $ buildUpdateArrayExpr sym xes ix newXe + pure $ XArray xes' + _ -> unexpectedValues "update array operation" + unexpectedValues :: forall m x . (Panic.HasCallStack, MonadIO m) => String -> m x unexpectedValues op = @@ -1128,6 +1211,52 @@ curIxExpr <- WI.bvLit sym knownNat (BV.word32 curIx) ixEq <- WI.bvEq sym curIxExpr ix mkIte sym ixEq xe rstExpr + +-- | Construct an expression that updates an array element at a particular index +-- by building a chain of @if@ expressions, where each expression checks if the +-- current index is equal to a given index in the array. If the indices are +-- equal, return the array with the element at that index updated. Otherwise, +-- proceed to the next @if@ expression, which checks the next index in the +-- array. +buildUpdateArrayExpr :: forall sym n. + (1 <= n, WFP.IsInterpretedFloatExprBuilder sym) + => sym + -> V.Vector n (XExpr sym) + -- ^ Elements + -> WI.SymBV sym 32 + -- ^ Index + -> XExpr sym + -- ^ New element + -> IO (V.Vector n (XExpr sym)) +buildUpdateArrayExpr sym xelts ix newXe = loop (knownNat @0) + where + n :: NatRepr n + n = V.length xelts + + n32 :: NatRepr 32 + n32 = knownNat @32 + + loop :: forall i. + ((i + 1) <= n) + => NatRepr i + -> IO (V.Vector n (XExpr sym)) + loop curIx = + case testStrictLeq nextIx n of + -- Recursive case + Left LeqProof -> do + rstExpr <- loop nextIx + curIxExpr <- WI.bvLit sym n32 $ BV.mkBV n32 $ intValue curIx + ixEq <- WI.bvEq sym curIxExpr ix + V.zipWithM (mkIte sym ixEq) newXelts rstExpr + -- Base case, we are at the last possible index (n - 1) + Right Refl -> + pure newXelts + where + nextIx :: NatRepr (i + 1) + nextIx = incNat curIx + + newXelts :: V.Vector n (XExpr sym) + newXelts = V.insertAt curIx newXe xelts -- | Construct an @if@ expression of the appropriate type. mkIte :: WFP.IsInterpretedFloatExprBuilder sym diff --git a/tests/Test/Copilot/Theorem/What4.hs b/tests/Test/Copilot/Theorem/What4.hs --- a/tests/Test/Copilot/Theorem/What4.hs +++ b/tests/Test/Copilot/Theorem/What4.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DataKinds #-} -- The following warning is disabled due to a necessary instance of SatResult -- defined in this module. {-# OPTIONS_GHC -fno-warn-orphans #-} @@ -6,17 +7,22 @@ -- External imports import Data.Int (Int8) +import Data.Word (Word32) import Test.Framework (Test, testGroup) import Test.Framework.Providers.QuickCheck2 (testProperty) -import Test.QuickCheck (Property, arbitrary, forAll) +import Test.QuickCheck (Arbitrary (arbitrary), Property, + arbitrary, forAll) import Test.QuickCheck.Monadic (monadicIO, run) -- External imports: Copilot -import Copilot.Core.Expr (Expr (Const, Op2)) -import Copilot.Core.Operators (Op2 (..)) +import Copilot.Core.Expr (Expr (Const, Op1, Op2)) +import Copilot.Core.Operators (Op1 (..), Op2 (..)) import Copilot.Core.Spec (Spec (..)) import qualified Copilot.Core.Spec as Copilot -import Copilot.Core.Type (Typed (typeOf)) +import Copilot.Core.Type (Field (..), + Struct (toValues, typeName), + Type (Struct), Typed (typeOf), + Value (..)) -- Internal imports: Modules being tested import Copilot.Theorem.What4 (SatResult (..), Solver (..), prove) @@ -30,6 +36,7 @@ [ testProperty "Prove via Z3 that true is valid" testProveZ3True , testProperty "Prove via Z3 that false is invalid" testProveZ3False , testProperty "Prove via Z3 that x == x is valid" testProveZ3EqConst + , testProperty "Prove via Z3 that a struct update is valid" testProveZ3StructUpdate ] -- * Individual tests @@ -76,6 +83,54 @@ spec :: Int8 -> Spec spec x = propSpec propName $ Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x) + +-- | Test that Z3 is able to prove the following expresion valid: +-- @ +-- for all (s :: MyStruct), +-- ((s ## testField =$ (+1)) # testField) == ((s # testField) + 1) +-- @ +testProveZ3StructUpdate :: Property +testProveZ3StructUpdate = forAll arbitrary $ \x -> + monadicIO $ run $ checkResult Z3 propName (spec x) Valid + where + propName :: String + propName = "prop" + + spec :: TestStruct -> Spec + spec s = propSpec propName $ + Op2 + (Eq typeOf) + (getField + (Op2 + (UpdateField typeOf typeOf testField) + sExpr + (add1 (getField sExpr)))) + (add1 (getField sExpr)) + where + sExpr :: Expr TestStruct + sExpr = Const typeOf s + + getField :: Expr TestStruct -> Expr Word32 + getField = Op1 (GetField typeOf typeOf testField) + + add1 :: Expr Word32 -> Expr Word32 + add1 x = Op2 (Add typeOf) x (Const typeOf 1) + +-- | A simple data type with a 'Struct' instance and a 'Field'. This is only +-- used as part of 'testProveZ3StructUpdate'. +newtype TestStruct = TestStruct { testField :: Field "testField" Word32 } + +instance Arbitrary TestStruct where + arbitrary = do + w32 <- arbitrary + return (TestStruct (Field w32)) + +instance Struct TestStruct where + typeName _ = "testStruct" + toValues s = [Value typeOf (testField s)] + +instance Typed TestStruct where + typeOf = Struct (TestStruct (Field 0)) -- | Check that the solver's satisfiability result for the given property in -- the given spec matches the expectation.