diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index 120e1e677..efc0d0bcf 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2024-08-30 + * Add support for struct updates in Copilot.Theorem.What4. (#524) + 2024-07-07 * Version bump (3.20). (#522) * What4 upper-bound dependency version bump. (#514) diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs index f55e3884e..5b84b021b 100644 --- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs +++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs @@ -799,6 +799,8 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of (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 +966,55 @@ translateOp2 sym origExpr op xe1 xe2 = case (op, xe1, xe2) of 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'. diff --git a/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs b/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs index 8297ba262..dbd98eb4a 100644 --- a/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs +++ b/copilot-theorem/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 @@ module Test.Copilot.Theorem.What4 where -- 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 @@ tests = [ 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 @@ -77,6 +84,54 @@ testProveZ3EqConst = forAll arbitrary $ \x -> 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. checkResult :: Solver -> String -> Spec -> SatResult -> IO Bool diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index a83f6135f..c71906891 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2024-08-30 + * Update example to demonstrate struct update support. (#524) + 2024-07-07 * Version bump (3.20). (#522) * Update README to reflect support for GHC 9.8. (#518) diff --git a/copilot/examples/what4/Structs.hs b/copilot/examples/what4/Structs.hs index de4e4efbd..fc61feadf 100644 --- a/copilot/examples/what4/Structs.hs +++ b/copilot/examples/what4/Structs.hs @@ -64,6 +64,10 @@ spec = do void $ prop "Example 2" $ forAll $ (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4) + -- Update a struct field, then check it for equality. + void $ prop "Example 3" $ forAll $ + ((battery ## temp =$ (+1))#temp == (battery#temp + 1)) + main :: IO () main = do spec' <- reify spec