Skip to content

Commit c8f4221

Browse files
RyanGlScottRyanGlScott
committed
copilot-verifier: Include in mainline copilot repo. Refs #622.
The `copilot-verifier` package was originally developed in an external repo (https://github.com/Copilot-Language/copilot-verifier), but there is interest in having all Copilot projects and libraries merged into the main https://github.com/Copilot-Language/copilot repo for ease of management. This commit includes the last state of the old `copilot-verified` repo into the main Copilot repo as a new subdirectory, disregarding the commit history.
1 parent fd769d4 commit c8f4221

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

46 files changed

+4734
-0
lines changed

‎copilot-verifier/CHANGELOG‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
2025-05-08
2+
* Version bump (4.4). (#85)
3+
4+
2025-03-10
5+
* Version bump (4.3). (#82)
6+
* Add `smtSolver` option to `VerifierOptions`. (#78)
7+
* Add `smtFloatMode` option to `VerifierOptions`. (#79)
8+
9+
2025-01-20
10+
* Version bump (4.2). (#76)
11+
* Reject specs that use multiple triggers with the same name. (#74)
12+
13+
2024-11-08
14+
* Version bump (4.1). (#72)
15+
16+
2024-09-09
17+
* Version bump (4.0). (#69)
18+
* Support verifying programs that use array updates. (#63)
19+
* Support verifying programs that use struct updates. (#57)
20+
21+
2024-08-03
22+
* Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`. (#64)
23+
* Support GHC 9.4 through 9.8. (#65)
24+
25+
2024-07-30
26+
* When using `Noisy` verbosity, always log proof goals related to the
27+
core correspondence proof, even if the goals are trivial. (#51)
28+
* When using `Noisy` verbosity, log more information about which proof
29+
goals arise before or after calling the `step()` function. (#52)
30+
31+
2024-07-11
32+
* Version bump (3.20). (#58)
33+
34+
2024-03-08
35+
* Version bump (3.19). (#53)
36+
* Provide more detailed feedback upon a successful run of the verifier.
37+
* Make the examples build with Copilot 3.19. (#53)
38+
39+
2024-02-06
40+
* Initial release of `copilot-verifier`.

‎copilot-verifier/LICENSE‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
Copyright (c) 2021-2024 Galois Inc.
2+
All rights reserved.
3+
4+
Redistribution and use in source and binary forms, with or without
5+
modification, are permitted provided that the following conditions
6+
are met:
7+
8+
* Redistributions of source code must retain the above copyright
9+
notice, this list of conditions and the following disclaimer.
10+
11+
* Redistributions in binary form must reproduce the above copyright
12+
notice, this list of conditions and the following disclaimer in
13+
the documentation and/or other materials provided with the
14+
distribution.
15+
16+
* Neither the name of Galois, Inc. nor the names of its contributors
17+
may be used to endorse or promote products derived from this
18+
software without specific prior written permission.
19+
20+
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
21+
IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
22+
TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
23+
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
24+
OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
25+
EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
26+
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
27+
PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
28+
LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
29+
NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
30+
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

‎copilot-verifier/README.md‎

Lines changed: 351 additions & 0 deletions
Large diffs are not rendered by default.

‎copilot-verifier/copilot-verifier.cabal‎

Lines changed: 152 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,152 @@
1+
Cabal-version: 2.2
2+
Name: copilot-verifier
3+
Version: 4.4
4+
Author: Galois Inc.
5+
Maintainer: rscott@galois.com
6+
Copyright: (c) Galois, Inc 2021-2024
7+
License: BSD-3-Clause
8+
License-file: LICENSE
9+
Build-type: Simple
10+
Category: Language
11+
Synopsis: System for verifying the correctness of generated Copilot programs
12+
Description:
13+
@copilot-verifier@ is an add-on to the [Copilot Stream
14+
DSL](https://copilot-language.github.io) for verifying the correctness of C
15+
code generated by the @copilot-c99@ package.
16+
.
17+
@copilot-verifier@ uses the [Crucible symbolic
18+
simulator](https://github.com/galoisinc/crucible) to interpret the semantics
19+
of the generated C program and and to produce verification conditions
20+
sufficient to guarantee that the meaning of the generated program corresponds
21+
in a precise way to the meaning of the original stream specification. The
22+
generated verification conditions are then dispatched to SMT solvers to be
23+
automatically solved.
24+
extra-doc-files: CHANGELOG, README.md
25+
26+
source-repository head
27+
type: git
28+
location: https://github.com/GaloisInc/copilot-verifier
29+
subdir: copilot-verifier
30+
31+
common bldflags
32+
ghc-options: -Wall
33+
-Werror=incomplete-patterns
34+
-Werror=missing-methods
35+
-Werror=overlapping-patterns
36+
-Wpartial-fields
37+
-Wincomplete-uni-patterns
38+
ghc-prof-options: -O2 -fprof-auto-exported
39+
default-language: Haskell2010
40+
default-extensions:
41+
NondecreasingIndentation
42+
build-depends:
43+
aeson >= 1.5 && < 2.3,
44+
base >= 4.8 && < 4.20,
45+
bv-sized >= 1.0.0 && < 1.1,
46+
bytestring,
47+
containers >= 0.5.9.0,
48+
copilot-c99 >= 4.4 && < 4.5,
49+
copilot-core >= 4.4 && < 4.5,
50+
copilot-theorem >= 4.4 && < 4.5,
51+
crucible >= 0.7.1 && < 0.8,
52+
crucible-llvm >= 0.7 && < 0.8,
53+
crux >= 0.7.1 && < 0.8,
54+
crux-llvm >= 0.9 && < 0.10,
55+
filepath,
56+
lens,
57+
llvm-pretty >= 0.12.1.0 && < 0.13,
58+
mtl,
59+
panic >= 0.3,
60+
parameterized-utils >= 2.1.4 && < 2.2,
61+
prettyprinter >= 1.7.0,
62+
text,
63+
transformers,
64+
vector,
65+
what4 >= 1.6.1 && < 1.7
66+
67+
library
68+
import: bldflags
69+
70+
hs-source-dirs: src
71+
exposed-modules:
72+
Copilot.Verifier
73+
Copilot.Verifier.FloatMode
74+
Copilot.Verifier.Log
75+
Copilot.Verifier.Solver
76+
77+
library copilot-verifier-examples
78+
import: bldflags
79+
80+
hs-source-dirs: examples
81+
build-depends:
82+
case-insensitive,
83+
copilot >= 4.4 && < 4.5,
84+
copilot-language >= 4.4 && < 4.5,
85+
copilot-libraries >= 4.4 && < 4.5,
86+
copilot-prettyprinter >= 4.4 && < 4.5,
87+
copilot-verifier
88+
exposed-modules:
89+
Copilot.Verifier.Examples
90+
91+
Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin
92+
Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap
93+
Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero
94+
Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds
95+
Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero
96+
Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap
97+
Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge
98+
Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge
99+
Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap
100+
101+
Copilot.Verifier.Examples.ShouldPass.Array
102+
Copilot.Verifier.Examples.ShouldPass.ArrayGen
103+
Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs
104+
Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument
105+
Copilot.Verifier.Examples.ShouldPass.Arith
106+
Copilot.Verifier.Examples.ShouldPass.Clock
107+
Copilot.Verifier.Examples.ShouldPass.Counter
108+
Copilot.Verifier.Examples.ShouldPass.Engine
109+
Copilot.Verifier.Examples.ShouldPass.FPNegation
110+
Copilot.Verifier.Examples.ShouldPass.FPOps
111+
Copilot.Verifier.Examples.ShouldPass.Heater
112+
Copilot.Verifier.Examples.ShouldPass.IntOps
113+
Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin
114+
Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap
115+
Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero
116+
Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds
117+
Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero
118+
Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap
119+
Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge
120+
Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge
121+
Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap
122+
Copilot.Verifier.Examples.ShouldPass.Structs
123+
Copilot.Verifier.Examples.ShouldPass.UpdateArray
124+
Copilot.Verifier.Examples.ShouldPass.UpdateStruct
125+
Copilot.Verifier.Examples.ShouldPass.Voting
126+
Copilot.Verifier.Examples.ShouldPass.WCV
127+
128+
executable verify-examples
129+
import: bldflags
130+
131+
hs-source-dirs: exe
132+
main-is: VerifyExamples.hs
133+
build-depends:
134+
case-insensitive,
135+
copilot-verifier,
136+
copilot-verifier-examples,
137+
optparse-applicative
138+
139+
test-suite copilot-verifier-test
140+
import: bldflags
141+
142+
type: exitcode-stdio-1.0
143+
hs-source-dirs: test
144+
build-depends:
145+
case-insensitive,
146+
copilot-verifier,
147+
copilot-verifier-examples,
148+
silently >= 1.2,
149+
tasty >= 0.10,
150+
tasty-expected-failure >= 0.12,
151+
tasty-hunit >= 0.10
152+
main-is: Test.hs

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

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
{-# LANGUAGE OverloadedStrings #-}
2+
module Copilot.Verifier.Examples
3+
( shouldFailExamples
4+
, shouldPassExamples
5+
) where
6+
7+
import qualified Data.CaseInsensitive as CI
8+
import Data.CaseInsensitive (CI)
9+
import qualified Data.Map as Map
10+
import Data.Map (Map)
11+
import Data.Text (Text)
12+
13+
import Copilot.Verifier (Verbosity)
14+
import qualified Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin as Fail.AbsIntMin
15+
import qualified Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap as Fail.AddSignedWrap
16+
import qualified Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero as Fail.DivByZero
17+
import qualified Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds as Fail.IndexOutOfBounds
18+
import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero as Fail.ModByZero
19+
import qualified Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap as Fail.MulSignedWrap
20+
import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge as Fail.ShiftLTooLarge
21+
import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge as Fail.ShiftRTooLarge
22+
import qualified Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap as Fail.SubSignedWrap
23+
import qualified Copilot.Verifier.Examples.ShouldPass.Array as Array
24+
import qualified Copilot.Verifier.Examples.ShouldPass.ArrayGen as ArrayGen
25+
import qualified Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs as ArrayOfStructs
26+
import qualified Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument as ArrayTriggerArgument
27+
import qualified Copilot.Verifier.Examples.ShouldPass.Arith as Arith
28+
import qualified Copilot.Verifier.Examples.ShouldPass.Clock as Clock
29+
import qualified Copilot.Verifier.Examples.ShouldPass.Counter as Counter
30+
import qualified Copilot.Verifier.Examples.ShouldPass.Engine as Engine
31+
import qualified Copilot.Verifier.Examples.ShouldPass.FPNegation as FPNegation
32+
import qualified Copilot.Verifier.Examples.ShouldPass.FPOps as FPOps
33+
import qualified Copilot.Verifier.Examples.ShouldPass.Heater as Heater
34+
import qualified Copilot.Verifier.Examples.ShouldPass.IntOps as IntOps
35+
import qualified Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin as Pass.AbsIntMin
36+
import qualified Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap as Pass.AddSignedWrap
37+
import qualified Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds as Pass.IndexOutOfBounds
38+
import qualified Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero as Pass.DivByZero
39+
import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero as Pass.ModByZero
40+
import qualified Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap as Pass.MulSignedWrap
41+
import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge as Pass.ShiftLTooLarge
42+
import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge as Pass.ShiftRTooLarge
43+
import qualified Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap as Pass.SubSignedWrap
44+
import qualified Copilot.Verifier.Examples.ShouldPass.Structs as Structs
45+
import qualified Copilot.Verifier.Examples.ShouldPass.UpdateArray as UpdateArray
46+
import qualified Copilot.Verifier.Examples.ShouldPass.UpdateStruct as UpdateStruct
47+
import qualified Copilot.Verifier.Examples.ShouldPass.Voting as Voting
48+
import qualified Copilot.Verifier.Examples.ShouldPass.WCV as WCV
49+
50+
shouldFailExamples :: Verbosity -> Map (CI Text) (IO ())
51+
shouldFailExamples verb = Map.fromList
52+
[ -- Partial operation tests
53+
example "AbsIntMin-fail" (Fail.AbsIntMin.verifySpec verb)
54+
, example "AddSignedWrap-fail" (Fail.AddSignedWrap.verifySpec verb)
55+
, example "DivByZero-fail" (Fail.DivByZero.verifySpec verb)
56+
, example "IndexOutOfBounds-fail" (Fail.IndexOutOfBounds.verifySpec verb)
57+
, example "ModByZero-fail" (Fail.ModByZero.verifySpec verb)
58+
, example "MulSignedWrap-fail" (Fail.MulSignedWrap.verifySpec verb)
59+
, example "ShiftLTooLarge-fail" (Fail.ShiftLTooLarge.verifySpec verb)
60+
, example "ShiftRTooLarge-fail" (Fail.ShiftRTooLarge.verifySpec verb)
61+
, example "SubSignedWrap-fail" (Fail.SubSignedWrap.verifySpec verb)
62+
]
63+
64+
shouldPassExamples :: Verbosity -> Map (CI Text) (IO ())
65+
shouldPassExamples verb = Map.fromList
66+
[ example "Array" (Array.verifySpec verb)
67+
, example "ArrayGen" (ArrayGen.verifySpec verb)
68+
, example "ArrayOfStructs" (ArrayOfStructs.verifySpec verb)
69+
, example "ArrayTriggerArgument" (ArrayTriggerArgument.verifySpec verb)
70+
, example "Arith" (Arith.verifySpec verb)
71+
, example "Clock" (Clock.verifySpec verb)
72+
, example "Counter" (Counter.verifySpec verb)
73+
, example "Engine" (Engine.verifySpec verb)
74+
, example "FPNegation" (FPNegation.verifySpec verb)
75+
, example "FPOps" (FPOps.verifySpec verb)
76+
, example "Heater" (Heater.verifySpec verb)
77+
, example "IntOps" (IntOps.verifySpec verb)
78+
, example "Structs" (Structs.verifySpec verb)
79+
, example "UpdateArray" (UpdateArray.verifySpec verb)
80+
, example "UpdateStruct" (UpdateStruct.verifySpec verb)
81+
, example "Voting" (Voting.verifySpec verb)
82+
, example "WCV" (WCV.verifySpec verb)
83+
84+
-- Partial operation tests
85+
, example "AbsIntMin-pass" (Pass.AbsIntMin.verifySpec verb)
86+
, example "AddSignedWrap-pass" (Pass.AddSignedWrap.verifySpec verb)
87+
, example "DivByZero-pass" (Pass.DivByZero.verifySpec verb)
88+
, example "IndexOutOfBounds-pass" (Pass.IndexOutOfBounds.verifySpec verb)
89+
, example "ModByZero-pass" (Pass.ModByZero.verifySpec verb)
90+
, example "MulSignedWrap-pass" (Pass.MulSignedWrap.verifySpec verb)
91+
, example "ShiftLTooLarge-pass" (Pass.ShiftLTooLarge.verifySpec verb)
92+
, example "ShiftRTooLarge-pass" (Pass.ShiftRTooLarge.verifySpec verb)
93+
, example "SubSignedWrap-pass" (Pass.SubSignedWrap.verifySpec verb)
94+
]
95+
96+
example :: Text -> IO () -> (CI Text, IO ())
97+
example name action = (CI.mk name, action)

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

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
{-# LANGUAGE NoImplicitPrelude #-}
2+
3+
-- | This will fail to verify since the verification does not assume the
4+
-- @notIntMin@ property, which is needed to prevent undefined behavior when
5+
-- invoking the 'abs' function.
6+
module Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin where
7+
8+
import Language.Copilot
9+
import Copilot.Compile.C99
10+
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
11+
, defaultVerifierOptions, verifyWithOptions )
12+
13+
spec :: Spec
14+
spec = do
15+
let stream :: Stream Int32
16+
stream = extern "stream" Nothing
17+
18+
_ <- prop "notIntMin" (forAll (stream > constI32 minBound))
19+
trigger "streamAbs" (abs stream == 1) [arg stream]
20+
21+
verifySpec :: Verbosity -> IO ()
22+
verifySpec verb = do
23+
spec' <- reify spec
24+
verifyWithOptions defaultVerifierOptions{verbosity = verb}
25+
mkDefaultCSettings
26+
-- ["notIntMin"]
27+
[]
28+
"absIntMinFail" spec'

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
{-# LANGUAGE NoImplicitPrelude #-}
2+
3+
-- | This will fail to verify since the verification does not assume the
4+
-- @notIntMax@ property, which is needed to prevent signed integer overflow.
5+
module Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap where
6+
7+
import Language.Copilot
8+
import Copilot.Compile.C99
9+
import Copilot.Verifier ( Verbosity, VerifierOptions(..)
10+
, defaultVerifierOptions, verifyWithOptions )
11+
12+
spec :: Spec
13+
spec = do
14+
let stream :: Stream Int32
15+
stream = extern "stream" Nothing
16+
17+
_ <- prop "notIntMax" (forAll (stream < constI32 maxBound))
18+
trigger "streamAddSigned" ((stream + 1) == 1) [arg stream]
19+
20+
verifySpec :: Verbosity -> IO ()
21+
verifySpec verb = do
22+
spec' <- reify spec
23+
verifyWithOptions defaultVerifierOptions{verbosity = verb}
24+
mkDefaultCSettings
25+
-- ["notIntMax"]
26+
[]
27+
"addSignedWrapFail" spec'

0 commit comments

Comments
 (0)