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.

Author: RyanGlScott

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