Add example demonstrating struct update support. Refs #57.

copilot-verifier/CHANGELOG

@@ -1,5 +1,6 @@
 2024-09-09
         * Support verifying programs that use array updates. (#63)
+        * Support verifying programs that use struct updates. (#57)
 
 2024-08-03
         * Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`. (#64)

copilot-verifier/copilot-verifier.cabal

@@ -117,6 +117,7 @@ library copilot-verifier-examples
     Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap
     Copilot.Verifier.Examples.ShouldPass.Structs
     Copilot.Verifier.Examples.ShouldPass.UpdateArray
+    Copilot.Verifier.Examples.ShouldPass.UpdateStruct
     Copilot.Verifier.Examples.ShouldPass.Voting
     Copilot.Verifier.Examples.ShouldPass.WCV
 

copilot-verifier/examples/Copilot/Verifier/Examples.hs

@@ -42,6 +42,7 @@ import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge   a
 import qualified Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap    as Pass.SubSignedWrap
 import qualified Copilot.Verifier.Examples.ShouldPass.Structs                  as Structs
 import qualified Copilot.Verifier.Examples.ShouldPass.UpdateArray              as UpdateArray
+import qualified Copilot.Verifier.Examples.ShouldPass.UpdateStruct             as UpdateStruct
 import qualified Copilot.Verifier.Examples.ShouldPass.Voting                   as Voting
 import qualified Copilot.Verifier.Examples.ShouldPass.WCV                      as WCV
 
@@ -74,6 +75,7 @@ shouldPassExamples verb = Map.fromList
     , example "IntOps" (IntOps.verifySpec verb)
     , example "Structs" (Structs.verifySpec verb)
     , example "UpdateArray" (UpdateArray.verifySpec verb)
+    , example "UpdateStruct" (UpdateStruct.verifySpec verb)
     , example "Voting" (Voting.verifySpec verb)
     , example "WCV" (WCV.verifySpec verb)
 

copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/UpdateStruct.hs

@@ -0,0 +1,62 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE DataKinds        #-}
+
+-- | An example showing of using @copilot-verifier@ to verify a specification
+-- involving structs where individual fields are updated.
+module Copilot.Verifier.Examples.ShouldPass.UpdateStruct where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+-- | Definition for `Volts`.
+data Volts = Volts
+  { numVolts :: Field "numVolts" Word32
+  , flag     :: Field "flag"     Bool
+  }
+
+-- | `Struct` instance for `Volts`.
+instance Struct Volts where
+  typeName _ = "volts"
+  toValues vlts = [ Value Word32 (numVolts vlts)
+                  , Value Bool   (flag vlts)
+                  ]
+
+-- | `Volts` instance for `Typed`.
+instance Typed Volts where
+  typeOf = Struct (Volts (Field 0) (Field False))
+
+data Battery = Battery
+  { temp  :: Field "temp"  Word32
+  , volts :: Field "volts" (Array 10 Volts)
+  , other :: Field "other" (Array 10 (Array 5 Word32))
+  }
+
+-- | `Battery` instance for `Struct`.
+instance Struct Battery where
+  typeName _ = "battery"
+  toValues battery = [ Value typeOf (temp battery)
+                     , Value typeOf (volts battery)
+                     , Value typeOf (other battery)
+                     ]
+
+-- | `Battery` instance for `Typed`. Note that `undefined` is used as an
+-- argument to `Field`. This argument is never used, so `undefined` will never
+-- throw an error.
+instance Typed Battery where
+  typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined))
+
+spec :: Spec
+spec = do
+  let battery :: Stream Battery
+      battery = extern "battery" Nothing
+
+  -- Update a struct field, then check it for equality.
+  trigger "updateTrig"
+    ((battery ## temp =$ (+1))#temp == (battery#temp + 1))
+    [arg battery]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "updateStruct"