From 4c76beaca05900fd23a48cc646b6723ddc38c916 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 9 Sep 2024 10:57:52 -0400 Subject: [PATCH 1/3] Require building with Copilot 4.0. Refs #63. The only code changes that were performed were in the `copilot-verifier` examples, which needed to update uses of `(.!!)` (which is now deprecated) to `(!)`, the modern equivalent introduced in Copilot 4.0. --- copilot-verifier/copilot-verifier.cabal | 12 ++++++------ .../Examples/ShouldFail/Partial/IndexOutOfBounds.hs | 2 +- .../Copilot/Verifier/Examples/ShouldPass/Array.hs | 2 +- .../Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs | 2 +- .../Verifier/Examples/ShouldPass/ArrayOfStructs.hs | 2 +- .../Copilot/Verifier/Examples/ShouldPass/Structs.hs | 6 +++--- 6 files changed, 13 insertions(+), 13 deletions(-) diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index 0008f1a..240e730 100644 --- a/copilot-verifier/copilot-verifier.cabal +++ b/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 diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs index 9e98acf..93f3812 100644 --- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs +++ b/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 diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs index 4a34e66..365d54c 100644 --- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs +++ b/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 () diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs index 3aa92ba..115c753 100644 --- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs +++ b/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 diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs index 9edc1ec..b983531 100644 --- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs +++ b/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 diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs index d778dd7..7f68e4b 100644 --- a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs +++ b/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 () From b4f297d7dcaa6fc7423b68bbb1a70b2be037d075 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 3 Sep 2024 09:56:20 -0400 Subject: [PATCH 2/3] Add example demonstrating array update support. Fixes #63. This is adapted from a similar example in the upstream `copilot` repo. --- copilot-verifier/copilot-verifier.cabal | 1 + .../examples/Copilot/Verifier/Examples.hs | 2 ++ .../Examples/ShouldPass/UpdateArray.hs | 32 +++++++++++++++++++ 3 files changed, 35 insertions(+) create mode 100644 copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/UpdateArray.hs diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index 240e730..1bac053 100644 --- a/copilot-verifier/copilot-verifier.cabal +++ b/copilot-verifier/copilot-verifier.cabal @@ -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 diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples.hs b/copilot-verifier/examples/Copilot/Verifier/Examples.hs index 919a047..d3ef537 100644 --- a/copilot-verifier/examples/Copilot/Verifier/Examples.hs +++ b/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) diff --git a/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/UpdateArray.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/UpdateArray.hs new file mode 100644 index 0000000..55a43b1 --- /dev/null +++ b/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" From 67816036cb71dc647a92813a99b85b1ef5bddf37 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 9 Sep 2024 11:11:20 -0400 Subject: [PATCH 3/3] Document changes in the CHANGELOG. Refs #63. --- copilot-verifier/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index 05e8c7e..0e51eae 100644 --- a/copilot-verifier/CHANGELOG +++ b/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)