Support array updates. Refs #63.

copilot-verifier/CHANGELOG

@@ -1,3 +1,6 @@
+2024-09-09
+        * Support verifying programs that use array updates. (#63)
+
 2024-08-03
         * Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`. (#64)
         * Support GHC 9.4 through 9.8. (#65)

copilot-verifier/copilot-verifier.cabal

@@ -45,9 +45,9 @@ common bldflags
     bv-sized >= 1.0.0 && < 1.1,
     bytestring,
     containers >= 0.5.9.0,
-    copilot-c99 >= 3.20 && < 3.21,
-    copilot-core >= 3.20 && < 3.21,
-    copilot-theorem >= 3.20 && < 3.21,
+    copilot-c99 >= 4.0 && < 4.1,
+    copilot-core >= 4.0 && < 4.1,
+    copilot-theorem >= 4.0 && < 4.1,
     crucible >= 0.7.1 && < 0.8,
     crucible-llvm >= 0.7 && < 0.8,
     crux >= 0.7.1 && < 0.8,
@@ -78,9 +78,9 @@ library copilot-verifier-examples
   hs-source-dirs: examples
   build-depends:
     case-insensitive,
-    copilot >= 3.20 && < 3.21,
-    copilot-language >= 3.20 && < 3.21,
-    copilot-prettyprinter >= 3.20 && < 3.21,
+    copilot >= 4.0 && < 4.1,
+    copilot-language >= 4.0 && < 4.1,
+    copilot-prettyprinter >= 4.0 && < 4.1,
     copilot-verifier
   exposed-modules:
     Copilot.Verifier.Examples
@@ -116,6 +116,7 @@ library copilot-verifier-examples
     Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge
     Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap
     Copilot.Verifier.Examples.ShouldPass.Structs
+    Copilot.Verifier.Examples.ShouldPass.UpdateArray
     Copilot.Verifier.Examples.ShouldPass.Voting
     Copilot.Verifier.Examples.ShouldPass.WCV
 

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

@@ -41,6 +41,7 @@ import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge   a
 import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge   as Pass.ShiftRTooLarge
 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.Voting                   as Voting
 import qualified Copilot.Verifier.Examples.ShouldPass.WCV                      as WCV
 
@@ -72,6 +73,7 @@ shouldPassExamples verb = Map.fromList
     , example "Heater" (Heater.verifySpec verb)
     , example "IntOps" (IntOps.verifySpec verb)
     , example "Structs" (Structs.verifySpec verb)
+    , example "UpdateArray" (UpdateArray.verifySpec verb)
     , example "Voting" (Voting.verifySpec verb)
     , example "WCV" (WCV.verifySpec verb)
 

copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs

@@ -19,7 +19,7 @@ spec = do
       stream2 = extern "stream2" Nothing
 
   _ <- prop "withinBounds" (forAll (stream2 < constW32 2))
-  trigger "streamIndex" ((stream1 .!! stream2) == 1) [arg stream1, arg stream2]
+  trigger "streamIndex" ((stream1 ! stream2) == 1) [arg stream1, arg stream2]
 
 verifySpec :: Verbosity -> IO ()
 verifySpec verb = do

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

@@ -31,7 +31,7 @@ spec = do
   -- It passes the current value of arr as an argument.
   -- The prototype of 'func' would be:
   -- void func (int8_t arg[3]);
-  trigger "func" (arr .!! 0) [arg arr]
+  trigger "func" (arr ! 0) [arg arr]
 
 -- Compile the spec
 verifySpec :: Verbosity -> IO ()

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

@@ -8,7 +8,7 @@ import Language.Copilot
 import qualified Prelude hiding ((++), (>))
 
 spec :: Spec
-spec = trigger "f" (stream .!! 0 > 0) [arg stream]
+spec = trigger "f" (stream ! 0 > 0) [arg stream]
   where
     stream :: Stream (Array 2 Int16)
     stream = [array [3,4]] ++ rest

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

@@ -17,7 +17,7 @@ instance Typed S where
   typeOf = Struct (S (Field 0))
 
 spec :: Spec
-spec = trigger "f" ((stream .!! 0)#field == 27) [arg stream]
+spec = trigger "f" ((stream ! 0)#field == 27) [arg stream]
   where
     stream :: Stream (Array 2 S)
     stream = [array [S (Field 27), S (Field 42)]] ++ stream

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

@@ -61,15 +61,15 @@ spec = do
   -- Check equality, indexing into nested structs and arrays. Note that this is
   -- trivial by equality.
   void $ prop "Example 1" $ forAll $
-    (((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts)
+    (((battery#volts) ! 0)#numVolts) == (((battery#volts) ! 0)#numVolts)
 
   -- Same as previous example, but get a different array index (so should be
   -- false).
   void $ prop "Example 2" $ forAll $
-    (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)
+    (((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4)
 
   -- Same as previous example, but in trigger form
-  trigger "otherTrig" ((((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4))
+  trigger "otherTrig" ((((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4))
                       [arg battery]
 
 verifySpec :: Verbosity -> IO ()

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

@@ -0,0 +1,32 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE DataKinds        #-}
+
+-- | An example showing of using @copilot-verifier@ to verify a specification
+-- involving arrays where individual elements are updated.
+module Copilot.Verifier.Examples.ShouldPass.UpdateArray where
+
+import Language.Copilot
+import Copilot.Compile.C99
+import Copilot.Verifier ( Verbosity, VerifierOptions(..)
+                        , defaultVerifierOptions, verifyWithOptions )
+
+spec :: Spec
+spec = do
+  let pair :: Stream (Array 2 Word32)
+      pair = extern "pair" Nothing
+
+  -- Check equality, indexing into array and modifying the value. Note that
+  -- this is trivial by equality.
+  trigger "trig_1"
+    (((pair !! 0 =$ (+1)) ! 0) == ((pair ! 0) + 1))
+    [arg pair]
+
+  -- Same as previous example, but get a different array index (so should be
+  -- false).
+  trigger "trig_2"
+    (((pair !! 0 =$ (+1)) ! 1) == ((pair ! 0) + 1))
+    [arg pair]
+
+verifySpec :: Verbosity -> IO ()
+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}
+                                                   mkDefaultCSettings [] "updateArray"