From d939de564d514b21f237c50be1e1fdcc220437bd Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 8 Jul 2024 08:15:31 -0400 Subject: [PATCH 1/5] copilot-theorem: Support translating `UpdateField` to what4. Refs #524. A new kind of `Op2`, called `UpdateField`, was added to `copilot-core` in a prior commit to support defining streams with updates to struct fields. This commit extends `copilot-theorem` to support reasoning about streams involving struct updates. We do so by providing a new case for the operation that translates a `copilot-core` `UpdateField` into a What4 representations of a Copilot expression. The implementation proves relatively straightforward, as struct field accessors always correspond to a concrete index value, which can then be used to update the value at the corresponding index in the list of struct fields. --- .../src/Copilot/Theorem/What4/Translate.hs | 51 +++++++++++++++++++ 1 file changed, 51 insertions(+) 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'. From 634b928862bcbc4db744ef9d2aa82e18781ea28d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 21 Aug 2024 11:22:01 -0400 Subject: [PATCH 2/5] copilot: Update example to demonstrate struct update support. Refs #524. This commit updates the `what4-structs` example in `copilot` (which depends on `copilot-theorem`) in order to demonstrate that `copilot-theorem` supports reasoning about a basic theorem involving a struct field update. --- copilot/examples/what4/Structs.hs | 4 ++++ 1 file changed, 4 insertions(+) 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 From 0ee80ccd9ce6a4856a4f551f590034fbc0c8def2 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 21 Aug 2024 11:51:17 -0400 Subject: [PATCH 3/5] copilot-theorem: Add a test case for struct updates. Refs #524. This adds a basic test case that ensures that applying a struct update followed by accessing the updated field is equivalent to accessing the field and then updating it. --- .../tests/Test/Copilot/Theorem/What4.hs | 63 +++++++++++++++++-- 1 file changed, 59 insertions(+), 4 deletions(-) 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 From 1818c721a8fea0e67b19954a90b21c4966d0adc9 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 21 Aug 2024 11:53:10 -0400 Subject: [PATCH 4/5] copilot-theorem: Document changes in CHANGELOG. Refs #524. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) 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) From bf0f4548f07484d8a262eba1784036ff17e5e3aa Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 30 Aug 2024 05:53:33 -0400 Subject: [PATCH 5/5] copilot: Document changes in CHANGELOG. Refs #524. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) 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)