copilot-verifier (empty) → 0.1

raw patch · 41 files changed

+4236/−0 lines, 41 filesdep +aesondep +basedep +bv-sized

Dependencies added: aeson, base, bv-sized, bytestring, case-insensitive, containers, copilot, copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-prettyprinter, copilot-theorem, copilot-verifier, crucible, crucible-llvm, crux, crux-llvm, filepath, lens, llvm-pretty, mtl, optparse-applicative, panic, parameterized-utils, prettyprinter, silently, tasty, tasty-expected-failure, tasty-hunit, text, transformers, vector, what4

Files

• CHANGELOG.md +5/−0
• LICENSE +30/−0
• README.md +327/−0
• copilot-verifier.cabal +146/−0
• examples/Copilot/Verifier/Examples.hs +91/−0
• examples/Copilot/Verifier/Examples/ShouldFail/Partial/AbsIntMin.hs +28/−0
• examples/Copilot/Verifier/Examples/ShouldFail/Partial/AddSignedWrap.hs +27/−0
• examples/Copilot/Verifier/Examples/ShouldFail/Partial/DivByZero.hs +27/−0
• examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs +31/−0
• examples/Copilot/Verifier/Examples/ShouldFail/Partial/ModByZero.hs +27/−0
• examples/Copilot/Verifier/Examples/ShouldFail/Partial/MulSignedWrap.hs +31/−0
• examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftLTooLarge.hs +32/−0
• examples/Copilot/Verifier/Examples/ShouldFail/Partial/ShiftRTooLarge.hs +32/−0
• examples/Copilot/Verifier/Examples/ShouldFail/Partial/SubSignedWrap.hs +27/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Arith.hs +52/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Array.hs +40/−0
• examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs +21/−0
• examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs +29/−0
• examples/Copilot/Verifier/Examples/ShouldPass/ArrayTriggerArgument.hs +23/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Clock.hs +46/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Counter.hs +56/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Engine.hs +44/−0
• examples/Copilot/Verifier/Examples/ShouldPass/FPOps.hs +88/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Heater.hs +60/−0
• examples/Copilot/Verifier/Examples/ShouldPass/IntOps.hs +64/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Partial/AbsIntMin.hs +19/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Partial/AddSignedWrap.hs +19/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Partial/DivByZero.hs +19/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Partial/IndexOutOfBounds.hs +19/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Partial/ModByZero.hs +19/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Partial/MulSignedWrap.hs +19/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Partial/ShiftLTooLarge.hs +19/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Partial/ShiftRTooLarge.hs +19/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Partial/SubSignedWrap.hs +19/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs +92/−0
• examples/Copilot/Verifier/Examples/ShouldPass/Voting.hs +64/−0
• examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs +194/−0
• exe/VerifyExamples.hs +53/−0
• src/Copilot/Verifier.hs +1517/−0
• src/Copilot/Verifier/Log.hs +729/−0
• test/Test.hs +32/−0

@@ -0,0 +1,5 @@+# Release history for copilot-verifier++## 0.1 (February 2024)++* Initial release of `copilot-verifier.

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

@@ -0,0 +1,327 @@+# Copilot Verifier++This "Copilot Verifier" is an add-on to the+[Copilot Stream DSL](https://copilot-language.github.io)+for verifying the correctness of C code generated+by the `copilot-c99` package.++The main idea of the verifier is to use the+[Crucible symbolic simulator](https://github.com/galoisinc/crucible)+to interpret the semantics of the generated C program and+and to produce verification conditions sufficient to guarantee+that the meaning of the generated program corresponds in a precise+way to the meaning of the original stream specification. The generated+verification conditions are then dispatched to SMT solvers to+be automatically solved.  We will have more to say about exactly+what is meant by this correspondence below.++## Building++To build the verifier from source, first make sure you have met the following+prerequisites:++* Ensure that you have the `cabal` and `ghc` executables in your `PATH`. If you+  don't already have them, we recommend using `ghcup` to install them:+  https://www.haskell.org/ghcup/. We recommend `Cabal` 3.10 or newer, and one of+  GHC 8.10, 9.2, or 9.4.++* Ensure that you have the `clang` and `llvm-link` utilities from LLVM in your+  `PATH`. Currently, LLVM versions up to 16 are supported. LLVM binaries are+  available at https://github.com/llvm/llvm-project/releases.++* Ensure that you have the `z3` SMT solver in your `PATH`. `z3` binaries are+  available at https://github.com/Z3Prover/z3/releases.++Then, clone the repo and run:++```+$ git submodule update --init+$ cabal test copilot-verifier+```++This will clone the repository, build the verifier, and run the associated test+suite. If you have performed all of the steps above correctly, the test suite+should pass.++## Using the Copilot Verifier++The main interface to the verifier is the `Copilot.Verifier.verify`+function, which takes some options to drive the code generation+process and a Copilot `Spec` object. It will invoke the Copilot+code generator to obtain C sources, compile the C sources into+LLVM bitcode using the `clang` compiler front-end, then+parse and interpret the bitcode using `crucible`.  After generating+verification conditions, it will dispatch them to an SMT solver,+and the result of those queries will be presented to the user.++There are a number of examples (based on similar examples+from the main Copilot repository) demonstrating how to+incorporate the verifier into a Copilot program.+See the `copilot-verifier/examples` subdirectory of this repository.++## Details of the Verification++### Synopsis of Copilot semantics++The Copilot DSL represents a certain nicely-behaved+class of discrete-time stream programs. Each `Stream`+in Copilot denotes an infinite stream of values; one may+just as well think that `Stream a` represents a pure mathematical+function `ℕ → a` from natural numbers to values of type `a`.+See the+[Copilot manual](https://ntrs.nasa.gov/api/citations/20200003164/downloads/20200003164.pdf)+for more details of the Copilot language itself and its semantics.++One of the central design considerations for Copilot is that is should+be possible to implement stream programs using a fixed, finite amount+of storage.  As a result, Copilot will only accept stream programs+that access a bounded amount of their input streams (including any+recursive stream references). This allows an+implementation strategy where the generated C code can use fixed-size+ring buffers to store a limited number of previous stream values.++The execution model for the generated programs is that the program+starts in a state corresponding to stream values at time `t = 0`;+"external" stream input values are placed in distinguished global+variables by the calling environment, which then executes a `step()`+function to move to the next time step.  The `step()` function captures+the values of these external inputs and does whatever computation is+necessary to update its internal state from time `t=n` to time+`t=n+1`.  In addition, it will call any defined "trigger" functions+if the stream state at that time step satisfies the defined guard condition.+In short, the generated C program steps one moment at a time through+the stream program, consuming a sequence of input values provided by+a cooperating environment and calling handler functions whenever+states of interest occur.++### The Desired Correspondence++What does it mean, then, for a generated C program in this style+to correctly implement a given stream program? The intuition+is basically that after `n` calls to the `step` function,+the state of the ring-buffers of the C program should correctly+compute the value of the corresponding stream expression+evaluated at index `n`, assuming the C program has been fed+inputs corresponding to the first `n` values of the external stream+inputs.  Moreover, the trigger functions should be called from+the `step` function exactly at the time values when the stream expressions+evaluate to true.++The notion of correspondence for the values flowing in streams is+relatively straightforward: these values consist of fixed-width+machine integers, floating-point values, structs and fixed-length+arrays. For each, the appropriate notion of equality is fairly clear.++Both the original `Stream` program and the generated C program+can be viewed straightforwardly as a transition system, and under+this view, the correspondence we want to establish is a bisimulation+between the states of the high-level stream program and the low-level+C program. The proof method for bisimulation requires us to provide+a "correspondence" relation between the program states, and then prove+three things about this relation:++1. that the initial states of the programs are in the relation;+2. if we assume two arbitrary program states begin in the relation+and each takes a single transition (consuming corresponding inputs),+the resulting states are back in the relation;+3. that any observable+actions taken by one program are exactly mirrored by the other.++On the high-level side of the bisimulation, the program+state is essentially just the value of the current time step `n`,+whereas on the C side it consists of the regions of global memory that+contain the ring-buffers and their current indices.  The transition+relation for the high-level program just increments the time value by+one, and the transition for the C program is defined by the action+of the generated `step()` function.++Suppose `s` is one of the stream definitions in the original Copilot+program which is required to retain `k` previous values;+let `buf` be the global variable name of the ring-buffer in the C+program, and `idx` be the global variable name maintaining the+current index into the ring buffer.  Then the correspondence+relation is basically that `0 <= idx < k` and+`s[n+i] = buf[(idx+i) mod k]` as `i` ranges from `0 .. k-1`.+By abuse of notation, here we mean that `s[j]` is+the value of the stream expression `s` evaluated at index `j`,+whereas `buf[j]` means the value obtained by reading the `j`th value+of the buffer `buf` from memory.  The overall correspondence relation+is a conjunction of statements like this, one for each stream+expression that is realized via a buffer.++### Implementing the Bisimulation proof steps++The kind of program correspondence property we desire is a largely+mechanical affair. As the code under consideration is automatically+generated, it has a very regular structure and is specifically+intended to implement the semantics we wich to verify it against.  As+such, we expect these proofs to be highly automatable.++The proof principle of bisimulation itself is not amenable+to reduction to SMT, as if falls outside the first-order theories+those solvers understand. Likewise, the semantics of Copilot+and C might possibly be reducible directly to SMT, but it would be+impractical to do so. However, we can reduce the individual+proof obligations mentioned above into a series of lower-level+logical statements that are amenable to SMT proof by+defining the logical semantics of stream programs, and using+symbolic simulation techniques to interpret the semantics of the+C program.  Performing this reduction is the key contribution+of `copilot-verifier`.++#### Initial state correspondence++The proof first obligation we must discharge is to show that+the initial states of the two programs correspond. For each+stream `s` there is a corresponding `k`, which is the length of+the ring-buffer implementing it.  We must simply verify that+the C program initializes its buffer with the first `k` values+of the stream `s`, and that the `idx` value starts at 0.+Because of the restrictions Copilot places on programs, these+first `k` values must be specified concretely and will not be+able to depend on any external inputs.  As such, this step+is quite easily performed, as it requires only direct evaluation+of concrete inputs.++#### Transition correspondence++The bulk of the proof effort consists of demonstrating that+the bisimulation relation is preserved by transitions.+In order to do this step, we must begin with totally symbolic+initial states: we know nothing except that we are at some+arbitrary time value `n`, and that the C program buffers+correspond to their stream values as required by the relation.+Thus, we create fresh symbolic variables for the streams+from `n` to `n + k-1`, and for the values of all the involved+external streams at time `n`. Then, we run forward the Copilot+program by evaluating the stream recurrence expression to+compute the value of each stream at time `n+k`.++Next we set up an initial state of the C program by choosing,+for each ring buffer, an arbitrary value for its current index+within its allowed range, and then writing the variables+corresponding to each stream value into the buffers at+their appropriate offsets. The symbolic simulator is then+invoked to compute the state update effects of the `step()`+function. Afterward, we read the poststate values from the+ring-buffers and verify that they correspond to the stream+values from `n+1` up to `n+k`.++As part of symbolic simulation, Crucible may also generate+side-conditions that relate to memory safety of the program, or to+error conditions that must be avoided. All of the bisimulation+equivalence conditions and the safety side-conditions will be+submitted to an SMT solver.++#### Observable effects++For our purposes, the only observable effects of a Copilot program+relate to any "trigger" functions defined in the spec.  Our task is to+show that the generated C code calls the external trigger functions if+and only if the corresponding guard condition is true, and that the+arguments passed to those functions are as expected.+This proof obligation is proved in the same phase along with+the transition relation proof above because the `step()` function+is responsible for both invoking triggers and for performing state+updates.++The technique we use to perform this aspect of the proof is to+install "override" functions to the external symbols corresponding+to the C trigger functions before we begin symbolic simulation.+In a real system, the external environment would be responsible+for implementing these functions and taking whatever appropriate+action is necessary when the triggers fire. However, we are verifying+the generated code in isolation from its environment, so we have no+implementation in hand. Instead, the override will+essentially implement a stub function that simply captures its+arguments and the path condition under which it was called.+After simulation completes, the captured arguments and path condition+are required to be equivalent to the corresponding trigger guard+and arguments from the Copilot spec.  These conditions are+discharged to the SMT solver at the same time as the transition+relation obligations.++Because of the way we model the trigger functions, we make a number of+implicit assumptions about how the actual implementations of those+functions must behave. The most important of those assumptions is that+the trigger functions must not modify any memory under the control of+the Copilot program, including its ring buffers and stack.  We also+assume that the trigger functions are well defined, i.e. they are+memory safe and do not perform any undefined behavior.++#### Partial operations++A generated C program may make use of partial operations. These range from+division, which can fail if the second argument is zero, to signed integer+arithmetic, which can overflow and result in undefined behavior. The verifier+has two modes for dealing with partial operations:++1. Any invocation of a partial operation on undefined inputs in the generated+   C program will result in an error, provided that the user did not add an+   assertion that assumes this behavior will not occur.++2. If the generated C program invokes a partial operation on undefined inputs,+   the verifier will check if this coincides with a corresponding invocation+   of a partial operation in the Copilot spec. If so, the verification will+   succeed. In other words, the verifier will check that the spec and the+   C program are "crash-equivalent".++The verifier uses mode (1) by default, but mode (2) can be enabled by using+`Copilot.Verifier.verifyWithOptions sideCondVerifierOptions`. In this mode,+the verifier will analyze any invocation of a operation which could be partial+and generate a side condition that this operation will only be invoked on+well defined inputs. During the transition step of the bisimulation proof,+the verifier will add these side conditions as assumptions. Therefore, if+simulating the C program generates any side conditions due to invoking partial+operations, these side conditions from the C program should be dischargeable+using the corresponding side conditions from the Copilot spec.++Mode (2) has the caveat that `clang` may compile C code to LLVM bitcode in+which a partial function is no longer applied to undefined inputs. For+instance, `clang` will sometimes promote 16-bit integer values to 32 bits+before performing arithmetic on them. This can turn an operation that would+result in signed 16-bit integer overflow into a 32-bit integer operation+that does _not_ overflow, for instance.++### Caveats About the Verifier++We rely on the `clang` compiler front-end to consume C source files+and produce LLVM intermediate language, which then becomes the input+to the later verification steps. To the extent that the input program+is not fully-portable C, `clang` may make implementation-specific+decisions about how to compile the program which might be made+different if compiled by a different compiler (e.g. `gcc`). We expect+this aspect to be mitigated by the fact that Copilot programs are+automatically generated into a rather simple subset of the C language,+and is designed to be as simple as possible.+Any code-generation bugs in `clang` itself may affect the soundness+of our verifier. Again, however, Copilot generates a well-understood+subset of the language, and we expect `clang` to be well-tested on+the code patterns produced.++The semantics of LLVM bitcode, as encoded in the `crucible-llvm`+package, may have errors that affect soundness. We mitigate this risk+by testing our semantics against a corpus of verification problems+produced for the SV-COMP verification competition, paying special+attention to any soundness issues that arise. `Crux`, a standalone+verification system based on `crucible-llvm`, was a participant in the+2022 edition of SV-COMP.++The semantics of Copilot programs, as encoded in the+`Copilot.Theorem.What4` module may have errors that affect soundness.+For the moment we do not have an effective mitigation strategy for+this risk other than manual examination and comparison against the+intended semantics of Copilot, as encoded in the interpreter.++There is limited SMT solver support for floating-point values,+especially for transcendental functions like the trig primitives.  As a+result, we reason about floating point expressions via uninterpreted+functions. In other words, we leave the semantics of the+floating-point operations totally abstract, and simply verify that the+Copilot program and the corresponding C program apply the same+operations in the same order. This is sound, but leaves the possibility+that the compiler will apply some correct transformation to+floating-point expressions that we are nonetheless unable to verify.+However, on low optimizations and without the `--fast-math` flag,+compilers generally (and `clang` in particular) are very reluctant to+rearrange floating-point code, and the verifications generally succeed.

@@ -0,0 +1,146 @@+Cabal-version: 2.2+Name:          copilot-verifier+Version:       0.1+Author:        Galois Inc.+Maintainer:    rscott@galois.com+Copyright:     (c) Galois, Inc 2021-2024+License:       BSD-3-Clause+License-file:  LICENSE+Build-type:    Simple+Category:      Language+Synopsis:      System for verifying the correctness of generated Copilot programs+Description:+  @copilot-verifier@ is an add-on to the <https://copilot-language.github.io+  Copilot Stream DSL> for verifying the correctness of C code generated by the+  @copilot-c99@ package.+  .+  @copilot-verifier@ uses the <https://github.com/galoisinc/crucible Crucible+  symbolic simulator> to interpret the semantics of the generated C program and+  and to produce verification conditions sufficient to guarantee that the+  meaning of the generated program corresponds in a precise way to the meaning+  of the original stream specification. The generated verification conditions+  are then dispatched to SMT solvers to be automatically solved.+extra-doc-files: CHANGELOG.md, README.md++source-repository head+  type:     git+  location: https://github.com/GaloisInc/copilot-verifier+  subdir:   copilot-verifier++common bldflags+  ghc-options: -Wall+               -Werror=incomplete-patterns+               -Werror=missing-methods+               -Werror=overlapping-patterns+               -Wpartial-fields+               -Wincomplete-uni-patterns+  ghc-prof-options: -O2 -fprof-auto-exported+  default-language: Haskell2010+  default-extensions:+     NondecreasingIndentation+  build-depends:+    aeson >= 1.5 && < 2.3,+    base >= 4.8 && < 4.18,+    bv-sized >= 1.0.0 && < 1.1,+    bytestring,+    containers >= 0.5.9.0,+    copilot >= 3.18.1 && < 3.19,+    copilot-c99 >= 3.18.1 && < 3.19,+    copilot-core >= 3.18.1 && < 3.19,+    copilot-libraries >= 3.18.1 && < 3.19,+    copilot-language >= 3.18.1 && < 3.19,+    copilot-prettyprinter >= 3.18.1 && < 3.19,+    copilot-theorem >= 3.18.1 && < 3.19,+    crucible >= 0.7 && < 0.8,+    crucible-llvm >= 0.6 && < 0.7,+    crux >= 0.7 && < 0.8,+    crux-llvm >= 0.8 && < 0.9,+    filepath,+    lens,+    llvm-pretty,+    mtl,+    panic >= 0.3,+    parameterized-utils >= 2.1.4 && < 2.2,+    prettyprinter >= 1.7.0,+    text,+    transformers,+    vector,+    what4 >= 0.4++library+  import: bldflags++  hs-source-dirs: src+  exposed-modules:+    Copilot.Verifier+    Copilot.Verifier.Log++library copilot-verifier-examples+  import: bldflags++  hs-source-dirs: examples+  build-depends:+    case-insensitive,+    copilot-verifier+  exposed-modules:+    Copilot.Verifier.Examples++    Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin+    Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap+    Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero+    Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds+    Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero+    Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap+    Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge+    Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge+    Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap++    Copilot.Verifier.Examples.ShouldPass.Array+    Copilot.Verifier.Examples.ShouldPass.ArrayGen+    Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs+    Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument+    Copilot.Verifier.Examples.ShouldPass.Arith+    Copilot.Verifier.Examples.ShouldPass.Clock+    Copilot.Verifier.Examples.ShouldPass.Counter+    Copilot.Verifier.Examples.ShouldPass.Engine+    Copilot.Verifier.Examples.ShouldPass.FPOps+    Copilot.Verifier.Examples.ShouldPass.Heater+    Copilot.Verifier.Examples.ShouldPass.IntOps+    Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin+    Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap+    Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero+    Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds+    Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero+    Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap+    Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge+    Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge+    Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap+    Copilot.Verifier.Examples.ShouldPass.Structs+    Copilot.Verifier.Examples.ShouldPass.Voting+    Copilot.Verifier.Examples.ShouldPass.WCV++executable verify-examples+  import: bldflags++  hs-source-dirs: exe+  main-is: VerifyExamples.hs+  build-depends:+    case-insensitive,+    copilot-verifier,+    copilot-verifier-examples,+    optparse-applicative++test-suite copilot-verifier-test+  import: bldflags++  type: exitcode-stdio-1.0+  hs-source-dirs: test+  build-depends:+    case-insensitive,+    copilot-verifier,+    copilot-verifier-examples,+    silently >= 1.2,+    tasty >= 0.10,+    tasty-expected-failure >= 0.12,+    tasty-hunit >= 0.10+  main-is: Test.hs

@@ -0,0 +1,91 @@+{-# LANGUAGE OverloadedStrings #-}+module Copilot.Verifier.Examples+  ( shouldFailExamples+  , shouldPassExamples+  ) where++import qualified Data.CaseInsensitive as CI+import Data.CaseInsensitive (CI)+import qualified Data.Map as Map+import Data.Map (Map)+import Data.Text (Text)++import Copilot.Verifier (Verbosity)+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin        as Fail.AbsIntMin+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap    as Fail.AddSignedWrap+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero        as Fail.DivByZero+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds as Fail.IndexOutOfBounds+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero        as Fail.ModByZero+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap    as Fail.MulSignedWrap+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge   as Fail.ShiftLTooLarge+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge   as Fail.ShiftRTooLarge+import qualified Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap    as Fail.SubSignedWrap+import qualified Copilot.Verifier.Examples.ShouldPass.Array                    as Array+import qualified Copilot.Verifier.Examples.ShouldPass.ArrayGen                 as ArrayGen+import qualified Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs           as ArrayOfStructs+import qualified Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument     as ArrayTriggerArgument+import qualified Copilot.Verifier.Examples.ShouldPass.Arith                    as Arith+import qualified Copilot.Verifier.Examples.ShouldPass.Clock                    as Clock+import qualified Copilot.Verifier.Examples.ShouldPass.Counter                  as Counter+import qualified Copilot.Verifier.Examples.ShouldPass.Engine                   as Engine+import qualified Copilot.Verifier.Examples.ShouldPass.FPOps                    as FPOps+import qualified Copilot.Verifier.Examples.ShouldPass.Heater                   as Heater+import qualified Copilot.Verifier.Examples.ShouldPass.IntOps                   as IntOps+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin        as Pass.AbsIntMin+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap    as Pass.AddSignedWrap+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds as Pass.IndexOutOfBounds+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero        as Pass.DivByZero+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero        as Pass.ModByZero+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap    as Pass.MulSignedWrap+import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge   as Pass.ShiftLTooLarge+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.Voting                   as Voting+import qualified Copilot.Verifier.Examples.ShouldPass.WCV                      as WCV++shouldFailExamples :: Verbosity -> Map (CI Text) (IO ())+shouldFailExamples verb = Map.fromList+    [ -- Partial operation tests+      example "AbsIntMin-fail" (Fail.AbsIntMin.verifySpec verb)+    , example "AddSignedWrap-fail" (Fail.AddSignedWrap.verifySpec verb)+    , example "DivByZero-fail" (Fail.DivByZero.verifySpec verb)+    , example "IndexOutOfBounds-fail" (Fail.IndexOutOfBounds.verifySpec verb)+    , example "ModByZero-fail" (Fail.ModByZero.verifySpec verb)+    , example "MulSignedWrap-fail" (Fail.MulSignedWrap.verifySpec verb)+    , example "ShiftLTooLarge-fail" (Fail.ShiftLTooLarge.verifySpec verb)+    , example "ShiftRTooLarge-fail" (Fail.ShiftRTooLarge.verifySpec verb)+    , example "SubSignedWrap-fail" (Fail.SubSignedWrap.verifySpec verb)+    ]++shouldPassExamples :: Verbosity -> Map (CI Text) (IO ())+shouldPassExamples verb = Map.fromList+    [ example "Array" (Array.verifySpec verb)+    , example "ArrayGen" (ArrayGen.verifySpec verb)+    , example "ArrayOfStructs" (ArrayOfStructs.verifySpec verb)+    , example "ArrayTriggerArgument" (ArrayTriggerArgument.verifySpec verb)+    , example "Arith" (Arith.verifySpec verb)+    , example "Clock" (Clock.verifySpec verb)+    , example "Counter" (Counter.verifySpec verb)+    , example "Engine" (Engine.verifySpec verb)+    , example "FPOps" (FPOps.verifySpec verb)+    , example "Heater" (Heater.verifySpec verb)+    , example "IntOps" (IntOps.verifySpec verb)+    , example "Structs" (Structs.verifySpec verb)+    , example "Voting" (Voting.verifySpec verb)+    , example "WCV" (WCV.verifySpec verb)++      -- Partial operation tests+    , example "AbsIntMin-pass" (Pass.AbsIntMin.verifySpec verb)+    , example "AddSignedWrap-pass" (Pass.AddSignedWrap.verifySpec verb)+    , example "DivByZero-pass" (Pass.DivByZero.verifySpec verb)+    , example "IndexOutOfBounds-pass" (Pass.IndexOutOfBounds.verifySpec verb)+    , example "ModByZero-pass" (Pass.ModByZero.verifySpec verb)+    , example "MulSignedWrap-pass" (Pass.MulSignedWrap.verifySpec verb)+    , example "ShiftLTooLarge-pass" (Pass.ShiftLTooLarge.verifySpec verb)+    , example "ShiftRTooLarge-pass" (Pass.ShiftRTooLarge.verifySpec verb)+    , example "SubSignedWrap-pass" (Pass.SubSignedWrap.verifySpec verb)+    ]++example :: Text -> IO () -> (CI Text, IO ())+example name action = (CI.mk name, action)

@@ -0,0 +1,28 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will fail to verify since the verification does not assume the+-- @notIntMin@ property, which is needed to prevent undefined behavior when+-- invoking the 'abs' function.+module Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = do+  let stream :: Stream Int32+      stream = extern "stream" Nothing++  _ <- prop "notIntMin" (forAll (stream > constI32 minBound))+  trigger "streamAbs" (abs stream == 1) [arg stream]++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    -- ["notIntMin"]+    []+    "absIntMinFail" spec'

@@ -0,0 +1,27 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will fail to verify since the verification does not assume the+-- @notIntMax@ property, which is needed to prevent signed integer overflow.+module Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = do+  let stream :: Stream Int32+      stream = extern "stream" Nothing++  _ <- prop "notIntMax" (forAll (stream < constI32 maxBound))+  trigger "streamAddSigned" ((stream + 1) == 1) [arg stream]++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    -- ["notIntMax"]+    []+    "addSignedWrapFail" spec'

@@ -0,0 +1,27 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will fail to verify since the verification does not assume the+-- @nonzero@ property, which is needed to prevent a division-by-zero error.+module Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = do+  let stream :: Stream Int16+      stream = extern "stream" Nothing++  _ <- prop "nonzero" (forAll (stream /= 0))+  trigger "streamDiv" ((stream `div` stream) == 1) [arg stream]++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    -- ["nonzero"]+    []+    "divByZeroFail" spec'

@@ -0,0 +1,31 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will fail to verify since the verification does not assume the+-- @withinBounds@ property, which is needed to prevent an out-of-bounds array index.+module Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = do+  let stream1 :: Stream (Array 2 Int16)+      stream1 = constant (array [27, 42])++      stream2 :: Stream Word32+      stream2 = extern "stream2" Nothing++  _ <- prop "withinBounds" (forAll (stream2 < constW32 2))+  trigger "streamIndex" ((stream1 .!! stream2) == 1) [arg stream1, arg stream2]++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    -- ["withinBounds"]+    []+    "indexFail" spec'

@@ -0,0 +1,27 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will fail to verify since the verification does not assume the+-- @nonzero@ property, which is needed to prevent a division-by-zero error.+module Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = do+  let stream :: Stream Int16+      stream = extern "stream" Nothing++  _ <- prop "nonzero" (forAll (stream /= 0))+  trigger "streamMod" ((stream `mod` stream) == 1) [arg stream]++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    -- ["nonzero"]+    []+    "modByZeroFail" spec'

@@ -0,0 +1,31 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will fail to verify since the verification does not assume the+-- @withinRange@ property, which is needed to prevent signed integer underflow or overflow.+module Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap where++import qualified Prelude as P++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = do+  let stream :: Stream Int32+      stream = extern "stream" Nothing++  _ <- prop "withinRange" (forAll+           (constI32 ((minBound P.+ 1) P.* 2) < stream+         && stream < constI32 ((maxBound P.- 1) `P.div` 2)))+  trigger "streamMulSigned" ((stream * 2) == 2) [arg stream]++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    -- ["withinRange"]+    []+    "mulSignedWrapFail" spec'

@@ -0,0 +1,32 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will fail to verify since the verification does not assume the+-- @lessThanBitWidth@ property, which is needed to prevent shifting by too+-- large of a value.+module Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = do+  let stream1 :: Stream Int32+      stream1 = extern "stream1" Nothing++      stream2 :: Stream Int64+      stream2 = extern "stream2" Nothing++  _ <- prop "lessThanBitWidth" (forAll+         (constI64 0 <= stream2 && stream2 < constI64 32))+  trigger "streamShiftL" ((stream1 .<<. stream2) == 1) [arg stream1, arg stream2]++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    -- ["lessThanBitWidth"]+    []+    "shiftLTooLargeFail" spec'

@@ -0,0 +1,32 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will fail to verify since the verification does not assume the+-- @lessThanBitWidth@ property, which is needed to prevent shifting by too+-- large of a value.+module Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = do+  let stream1 :: Stream Int32+      stream1 = extern "stream1" Nothing++      stream2 :: Stream Int64+      stream2 = extern "stream2" Nothing++  _ <- prop "lessThanBitWidth" (forAll+         (constI64 0 <= stream2 && stream2 < constI64 32))+  trigger "streamShiftR" ((stream1 .<<. stream2) == 1) [arg stream1, arg stream2]++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    -- ["lessThanBitWidth"]+    []+    "shiftRTooLargeFail" spec'

@@ -0,0 +1,27 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will fail to verify since the verification does not assume the+-- @notIntMin@ property, which is needed to prevent signed integer underflow.+module Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = do+  let stream :: Stream Int32+      stream = extern "stream" Nothing++  _ <- prop "notIntMin" (forAll (stream > constI32 minBound))+  trigger "streamSubSigned" ((stream - 1) == 1) [arg stream]++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    -- ["notIntMin"]+    []+    "subSignedWrapFail" spec'

@@ -0,0 +1,52 @@++{-# LANGUAGE RebindableSyntax #-}++module Copilot.Verifier.Examples.ShouldPass.Arith where++import Control.Monad (when)+import qualified Prelude as P++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )+import Copilot.Theorem.What4 (prove, Solver(..))++-- The largest unsigned 32-bit prime+lastPrime :: Stream Word32+lastPrime = 31+--lastPrime = 4294967291 -- Whelp, this prime seems too big for the solvers to handle well++multRingSpec :: Spec+multRingSpec = do+  _ <- prop "clamp nonzero" (forAll ((clamp > 0) && (clamp < lastPrime)))+  _ <- prop "reduced" (forAll (acc < lastPrime))+  _ <- prop "nonzero" (forAll (acc > 0 && (acc < lastPrime)))++  trigger "outofrange" (not (acc > 0 && acc < lastPrime)) [arg acc]++  return ()++  where+  -- a stream of external values+  vals  = externW32 "values" Nothing++  -- Generate a value in [1, lastPrime), which+  -- is the multiplictive group of Z_p+  clamp :: Stream Word32+  clamp = (vals `mod` (lastPrime - 1)) + 1++  -- Successively multiply new values+  acc :: Stream Word32+  acc = [1] ++ unsafeCast ((cast acc * cast clamp) `mod` (cast lastPrime :: Stream Word64))++verifySpec :: Verbosity -> IO ()+verifySpec verb =+  do s <- reify multRingSpec+     r <- prove Z3 s+     when (verb P.>= Default) $+       print r+     verifyWithOptions defaultVerifierOptions{verbosity = verb}+                       mkDefaultCSettings ["reduced"] "multRingSpec" s++--verifySpec _ = interpret 10 engineMonitor

@@ -0,0 +1,40 @@+--------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | This is a simple example for arrays. As a program, it does not make much+-- sense, however it shows of the features of arrays nicely.++-- | Enable compiler extension for type-level data, necesary for the array+-- length.++{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE DataKinds        #-}++module Copilot.Verifier.Examples.ShouldPass.Array where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++-- Lets define an array of length 2.+-- Make the buffer of the streams 3 elements long.+arr :: Stream (Array 2 Bool)+arr = [ array [True, False]+      , array [True, True]+      , array [False, False]] ++ arr++spec :: Spec+spec = do+  -- A trigger that fires 'func' when the first element of 'arr' is True.+  -- 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]++-- Compile the spec+verifySpec :: Verbosity -> IO ()+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}+                                                   mkDefaultCSettings [] "array"+-- verifySpec _ = interpret 30 spec

@@ -0,0 +1,21 @@+{-# LANGUAGE DataKinds #-}+module Copilot.Verifier.Examples.ShouldPass.ArrayGen where++import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )+import Language.Copilot+import qualified Prelude hiding ((++), (>))++spec :: Spec+spec = trigger "f" (stream .!! 0 > 0) [arg stream]+  where+    stream :: Stream (Array 2 Int16)+    stream = [array [3,4]] ++ rest++    rest :: Stream (Array 2 Int16)+    rest = constant $ array [5,6]++verifySpec :: Verbosity -> IO ()+verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}+                                                   mkDefaultCSettings [] "arrayGen"

@@ -0,0 +1,29 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE NoImplicitPrelude #-}+module Copilot.Verifier.Examples.ShouldPass.ArrayOfStructs where++import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )+import Language.Copilot++data S = S { field :: Field "field" Int16 }++instance Struct S where+  typename _ = "s"+  toValues s = [Value Int16 (field s)]++instance Typed S where+  typeOf = Struct (S (Field 0))++spec :: Spec+spec = trigger "f" ((stream .!! 0)#field == 27) [arg stream]+  where+    stream :: Stream (Array 2 S)+    stream = [array [S (Field 27), S (Field 42)]] ++ stream++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+                    mkDefaultCSettings [] "arrayOfStructs" spec'

@@ -0,0 +1,23 @@+{-# LANGUAGE DataKinds #-}++-- | A regression test for+-- <https://github.com/Copilot-Language/copilot/issues/431>.+module Copilot.Verifier.Examples.ShouldPass.ArrayTriggerArgument where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++spec :: Spec+spec = trigger "f" true [arg stream]+  where+    stream :: Stream (Array 2 Int16)+    stream = constant (array [3,4])++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions+    defaultVerifierOptions{verbosity = verb}+    mkDefaultCSettings [] "arrayTriggerArgument" spec'

@@ -0,0 +1,46 @@+--------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Example showing usage of clocks to generate periodically recurring truth+-- values.++module Copilot.Verifier.Examples.ShouldPass.Clock where++import Control.Monad (when)+import qualified Prelude as P++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )+import Copilot.Theorem.What4 (prove, Solver(..))++-- | We need to force a type for the argument of `period`.+p :: Word8+p = 5++-- | Both have the same period, but a different phase.+clkStream :: Stream Bool+clkStream  = clk (period p) (phase 0)++clkStream' :: Stream Bool+clkStream' = clk (period p) (phase 2)++spec :: Spec+spec = do+  observer "clk"  clkStream+  observer "clk'" clkStream'+  _ <- prop "clksPhase" (forAll (clkStream == drop 2 clkStream'))+  _ <- prop "clksDistinct" (forAll (not (clkStream && clkStream')))+  trigger "clksHigh" (clkStream && clkStream') []+++verifySpec :: Verbosity -> IO ()+verifySpec verb =+  do s <- reify spec+     r <- prove Z3 s+     when (verb P.>= Default) $+       print r+     verifyWithOptions defaultVerifierOptions{verbosity = verb}+                       mkDefaultCSettings [] "clock" s

@@ -0,0 +1,56 @@+-------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Example showing an implementation of a resettable counter.++{-# LANGUAGE RebindableSyntax #-}++module Copilot.Verifier.Examples.ShouldPass.Counter where++import Control.Monad (when)+import qualified Prelude as P++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )+import Copilot.Theorem.What4 (prove, Solver(..))++-- A resettable counter+counter :: (Typed a, Integral a) => Stream Bool -> Stream Bool -> Stream a+counter inc reset = cnt+  where+    cnt = if reset then 0+          else if inc then z + 1+               else z+    z = [0] ++ cnt++-- Counter that resets when it reaches 256+bytecounter :: Stream Int32+bytecounter = counter true (resetcounter `mod` 256 == 0)++resetcounter :: Stream Word32+resetcounter = counter true false++bytecounter2 :: Stream Int32+bytecounter2 = counter true ([False] ++ bytecounter2 == 255)++spec :: Spec+spec =+  do _ <- prop "range" (forAll (bytecounter == unsafeCast (resetcounter `mod` 256)))+     _ <- prop "range2" (forAll (0 <= bytecounter2 && bytecounter2 <= 255))+     _ <- prop "same"  (forAll ((0 <= bytecounter2 && bytecounter2 <= 255) &&+                                (bytecounter == unsafeCast (resetcounter `mod` 256)) &&+                                (bytecounter == bytecounter2)))+     trigger "counter" true [arg $ bytecounter, arg $ bytecounter2]++verifySpec :: Verbosity -> IO ()+-- verifSpec _ = interpret 1280 spec+verifySpec verb =+  do s <- reify spec+     r <- prove Z3 s+     when (verb P.>= Default) $+       print r+     verifyWithOptions defaultVerifierOptions{verbosity = verb}+                       mkDefaultCSettings ["range", "range2"] "counter" s

@@ -0,0 +1,44 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Example implementing an engine cooling control system.++{-# LANGUAGE RebindableSyntax #-}++module Copilot.Verifier.Examples.ShouldPass.Engine where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++import qualified Prelude as P++{- If the majority of the engine temperature probes exeeds 250 degrees, then+ - the cooler is engaged and remains engaged until the majority of the engine+ - temperature probes drop to 250 or below.  Otherwise, trigger an immediate+ - shutdown of the engine.+-}++engineMonitor :: Spec+engineMonitor = do+  trigger "shutoff" (not ok) [arg maj]++  where+  vals     = [ externW8 "tmp_probe_0" two51+             , externW8 "tmp_probe_1" two51+             , externW8 "tmp_probe_2" zero]+  exceed   = map (> 250) vals+  maj      = majority exceed+  checkMaj = aMajority exceed maj+  ok       = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler)++  two51  = Just $ [251, 251] P.++ repeat (250 :: Word8)+  zero   = Just $ repeat (0 :: Word8)+  cooler = Just $ [True, True] P.++ repeat False++verifySpec :: Verbosity -> IO ()+verifySpec verb = reify engineMonitor >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}+                                                            mkDefaultCSettings [] "engine"+--verifySpec _ = interpret 10 engineMonitor

@@ -0,0 +1,88 @@+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+module Copilot.Verifier.Examples.ShouldPass.FPOps where++import Copilot.Compile.C99 (mkDefaultCSettings)+import qualified Copilot.Language.Stream as Copilot+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )+import Data.Proxy (Proxy(..))+import Language.Copilot+import qualified Prelude as P++mkSpecFor :: forall a proxy. (RealFloat a, Typed a) => proxy a -> String -> Spec+mkSpecFor _ nameSuffix = do+  let mkName :: String -> String+      mkName namePrefix = namePrefix P.++ nameSuffix++      stream :: Stream a+      stream = extern (mkName "stream") Nothing++  triggerOp1 (mkName "abs") abs stream+  triggerOp1 (mkName "signum") signum stream+  triggerOp1 (mkName "recip") recip stream+  triggerOp1 (mkName "exp") exp stream+  triggerOp1 (mkName "sqrt") sqrt stream+  triggerOp1 (mkName "log") log stream+  triggerOp1 (mkName "sin") sin stream+  triggerOp1 (mkName "tan") tan stream+  triggerOp1 (mkName "cos") cos stream+  triggerOp1 (mkName "asin") asin stream+  triggerOp1 (mkName "atan") atan stream+  triggerOp1 (mkName "acos") acos stream+  triggerOp1 (mkName "sinh") sinh stream+  triggerOp1 (mkName "tanh") tanh stream+  triggerOp1 (mkName "cosh") cosh stream+  triggerOp1 (mkName "asinh") asinh stream+  triggerOp1 (mkName "atanh") atanh stream+  triggerOp1 (mkName "acosh") acosh stream+  triggerOp1 (mkName "ceiling") Copilot.ceiling stream+  triggerOp1 (mkName "floor") Copilot.floor stream++  triggerOp2 (mkName "add") (+) stream+  triggerOp2 (mkName "sub") (-) stream+  triggerOp2 (mkName "mul") (*) stream+  triggerOp2 (mkName "div") (/) stream+  triggerOp2 (mkName "pow") (**) stream+  triggerOp2 (mkName "logBase") logBase stream+  triggerOp2 (mkName "atan2") Copilot.atan2 stream++spec :: Spec+spec = do+  mkSpecFor (Proxy @Float) "F"+  mkSpecFor (Proxy @Double) "D"++triggerOp1 :: (RealFloat a, Typed a) =>+              String ->+              (Stream a -> Stream a) ->+              Stream a ->+              Spec+triggerOp1 name op stream =+  trigger (name P.++ "Trigger") (testOp1 op stream) [arg stream]++triggerOp2 :: (RealFloat a, Typed a) =>+              String ->+              (Stream a -> Stream a -> Stream a) ->+              Stream a ->+              Spec+triggerOp2 name op stream =+  trigger (name P.++ "Trigger") (testOp2 op stream) [arg stream]++testOp1 :: (RealFloat a, Typed a) =>+           (Stream a -> Stream a) -> Stream a -> Stream Bool+testOp1 op stream =+  -- NB: Use (>=) rather than (==) here, as floating-point equality gets weird+  -- due to NaNs.+  op stream >= op stream++testOp2 :: (RealFloat a, Typed a) =>+           (Stream a -> Stream a -> Stream a) -> Stream a -> Stream Bool+testOp2 op stream =+  op stream stream >= op stream stream++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+                    mkDefaultCSettings [] "fpOps" spec'

@@ -0,0 +1,60 @@+--------------------------------------------------------------------------------+-- Copyright 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- This is a simple example with basic usage. It implements a simple home+-- heating system: It heats when temp gets too low, and stops when it is high+-- enough. It read temperature as a byte (range -50C to 100C) and translates+-- this to Celcius.++module Copilot.Verifier.Examples.ShouldPass.Heater where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.PrettyPrint as PP+--import Copilot.Language.Prelude++import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++import qualified Prelude as P+import Control.Monad (when)++-- External temperature as a byte, range of -50C to 100C+temp :: Stream Word8+temp = extern "temperature" Nothing++-- Calculate temperature in Celcius.+-- We need to cast the Word8 to a Float. Note that it is an unsafeCast, as there+-- is no direct relation between Word8 and Float.+ctemp :: Stream Float+ctemp = (unsafeCast temp * constant (150.0/255.0)) - constant 50.0++-- width of the sliding window+window :: Int+window = 5++-- Compute the sliding average of the last 5 temps+-- (Here, 19.5 is the average of 18.0 and 21.0, the two temperature extremes+-- that we check for in the spec.)+avgTemp :: Stream Float+avgTemp = (sum window (replicate window 19.5 ++ ctemp)) / fromIntegral window++spec :: Spec+spec = do+  trigger "heaton"  (avgTemp < 18.0) [arg avgTemp]+  trigger "heatoff" (avgTemp > 21.0) [arg avgTemp]++-- Compile the spec+verifySpec :: Verbosity -> IO ()+verifySpec verb =+  do rspec <- reify spec+     when (verb P.>= Default) $ putStrLn (PP.prettyPrint rspec)+     verifyWithOptions defaultVerifierOptions{verbosity = verb}+                       mkDefaultCSettings [] "heater"+                       rspec++{-+  do spec' <- reify spec+     putStrLn $ prettyPrintDot spec'+-}

@@ -0,0 +1,64 @@+{-# LANGUAGE NoImplicitPrelude #-}+module Copilot.Verifier.Examples.ShouldPass.IntOps where++import Copilot.Compile.C99 (mkDefaultCSettings)+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )+import Language.Copilot+import qualified Prelude as P++spec :: Spec+spec = do+  let stream :: Stream Int16+      stream = extern "stream" Nothing++      shiftBy :: Stream Int16+      shiftBy = extern "shiftBy" Nothing++  _ <- prop "nonzero" (forAll (stream /= 0))+  _ <- prop "shiftByBits" (forAll (0 <= shiftBy && shiftBy < 16))++  triggerOp1 "abs" abs stream+  triggerOp1 "signum" signum stream+  triggerOp1 "bwNot" complement stream++  triggerOp2 "add" (+) stream stream+  triggerOp2 "sub" (-) stream stream+  triggerOp2 "mul" (*) stream stream+  triggerOp2 "mod" mod stream stream+  triggerOp2 "div" div stream stream+  triggerOp2 "bwAnd" (.&.) stream stream+  triggerOp2 "bwOr" (.|.) stream stream+  triggerOp2 "bwXor" (.^.) stream stream+  triggerOp2 "bwShiftL" (.<<.) stream shiftBy+  triggerOp2 "bwShiftR" (.>>.) stream shiftBy++triggerOp1 :: String ->+              (Stream Int16 -> Stream Int16) ->+              Stream Int16 ->+              Spec+triggerOp1 name op stream =+  trigger (name P.++ "Trigger") (testOp1 op stream) [arg stream]++triggerOp2 :: String ->+              (Stream Int16 -> Stream Int16 -> Stream Int16) ->+              Stream Int16 -> Stream Int16 ->+              Spec+triggerOp2 name op stream1 stream2 =+  trigger (name P.++ "Trigger") (testOp2 op stream1 stream2) [arg stream1, arg stream2]++testOp1 :: (Stream Int16 -> Stream Int16) -> Stream Int16 -> Stream Bool+testOp1 op stream =+  op stream == op stream++testOp2 :: (Stream Int16 -> Stream Int16 -> Stream Int16) ->+           Stream Int16 -> Stream Int16 ->+           Stream Bool+testOp2 op stream1 stream2 =+  op stream1 stream2 == op stream1 stream2++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+                    mkDefaultCSettings ["nonzero", "shiftByBits"] "intOps" spec'

@@ -0,0 +1,19 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Abs@+-- operation is well defined precisely when C's @abs@ function is well defined.+module Copilot.Verifier.Examples.ShouldPass.Partial.AbsIntMin where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , sideCondVerifierOptions, verifyWithOptions )+import Copilot.Verifier.Examples.ShouldFail.Partial.AbsIntMin (spec)++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    []+    "absIntMinPass" spec'

@@ -0,0 +1,19 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Add@+-- operation should overflow on signed integers precisely when C addition does.+module Copilot.Verifier.Examples.ShouldPass.Partial.AddSignedWrap where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , sideCondVerifierOptions, verifyWithOptions )+import Copilot.Verifier.Examples.ShouldFail.Partial.AddSignedWrap (spec)++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    []+    "addSignedWrapPass" spec'

@@ -0,0 +1,19 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Div@+-- operation is well defined precisely when C division is well defined.+module Copilot.Verifier.Examples.ShouldPass.Partial.DivByZero where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , sideCondVerifierOptions, verifyWithOptions )+import Copilot.Verifier.Examples.ShouldFail.Partial.DivByZero (spec)++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    []+    "divByZeroPass" spec'

@@ -0,0 +1,19 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will succeed with 'sideCondVerifierOptions', as Copilot's indexing+-- operation should be out of bounds precisely when C array indexes are out of bounds.+module Copilot.Verifier.Examples.ShouldPass.Partial.IndexOutOfBounds where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , sideCondVerifierOptions, verifyWithOptions )+import Copilot.Verifier.Examples.ShouldFail.Partial.IndexOutOfBounds (spec)++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    []+    "indexPass" spec'

@@ -0,0 +1,19 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Mod@+-- operation is well defined precisely when C's @%@ operator is well defined.+module Copilot.Verifier.Examples.ShouldPass.Partial.ModByZero where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , sideCondVerifierOptions, verifyWithOptions )+import Copilot.Verifier.Examples.ShouldFail.Partial.ModByZero (spec)++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    []+    "modByZeroPass" spec'

@@ -0,0 +1,19 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Mul@+-- operation should wrap on signed integers precisely when C multiplication does.+module Copilot.Verifier.Examples.ShouldPass.Partial.MulSignedWrap where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , sideCondVerifierOptions, verifyWithOptions )+import Copilot.Verifier.Examples.ShouldFail.Partial.MulSignedWrap (spec)++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    []+    "mulSignedWrapPass" spec'

@@ -0,0 +1,19 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @BwShiftL@+-- operation should only accept second arguments as large as C's @<<@ operation does.+module Copilot.Verifier.Examples.ShouldPass.Partial.ShiftLTooLarge where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , sideCondVerifierOptions, verifyWithOptions )+import Copilot.Verifier.Examples.ShouldFail.Partial.ShiftLTooLarge (spec)++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    []+    "shiftLTooLargePass" spec'

@@ -0,0 +1,19 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @BwShiftR@+-- operation should only accept second arguments as large as C's @>>@ operation does.+module Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , sideCondVerifierOptions, verifyWithOptions )+import Copilot.Verifier.Examples.ShouldFail.Partial.ShiftRTooLarge (spec)++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    []+    "shiftRTooLargePass" spec'

@@ -0,0 +1,19 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- | This will succeed with 'sideCondVerifierOptions', as Copilot's @Sub@+-- operation should underflow on signed integers precisely when C subtraction does.+module Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , sideCondVerifierOptions, verifyWithOptions )+import Copilot.Verifier.Examples.ShouldFail.Partial.SubSignedWrap (spec)++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions sideCondVerifierOptions{verbosity = verb}+    mkDefaultCSettings+    []+    "subSignedWrapPass" spec'

@@ -0,0 +1,92 @@+-- | An example showing the usage of the What4 backend in copilot-theorem for+-- structs and arrays. Particular focus is on nested structs.+-- For general usage of structs, refer to the general structs example.++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE NoImplicitPrelude #-}+module Copilot.Verifier.Examples.ShouldPass.Structs where++import Control.Monad (void, forM_, when)+import qualified Prelude as P++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Theorem.What4+import Copilot.Verifier ( Verbosity(..), VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )+++-- | Definition for `Volts`.+data Volts = Volts+  { numVolts :: Field "numVolts" Word16+  , flag     :: Field "flag"     Bool+  }++-- | `Struct` instance for `Volts`.+instance Struct Volts where+  typename _ = "volts"+  toValues vlts = [ Value Word16 (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"  Word16+  , 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++  -- 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)++  -- 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)++  -- Same as previous example, but in trigger form+  trigger "otherTrig" ((((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4))+                      [arg battery]++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec++  -- Use Z3 to prove the properties.+  results <- prove Z3 spec'++  -- Print the results.+  when (verb P.>= Default) $+    forM_ results $ \(nm, res) -> do+      putStr $ nm <> ": "+      case res of+        Valid   -> putStrLn "valid"+        Invalid -> putStrLn "invalid"+        Unknown -> putStrLn "unknown"++  verifyWithOptions defaultVerifierOptions{verbosity = verb}+                    mkDefaultCSettings [] "structs" spec'

@@ -0,0 +1,64 @@+--------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | Fault-tolerant voting examples.++{-# LANGUAGE RebindableSyntax #-}++module Copilot.Verifier.Examples.ShouldPass.Voting where++import Language.Copilot+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++vote :: Spec+vote = do+  -- majority selects element with the biggest occurance.+  trigger "maj"  true [arg maj]++  -- aMajority checks if the selected element has a majority.+  trigger "aMaj" true [arg $ aMajority inputs maj]++  where+    maj = majority inputs++    -- 26 input streams to vote on+    inputs :: [Stream Word32]+    inputs = [ a, b, c, d, e, f, g, h, i, j, k, l, m+             -- , n, o, p, q, r, s, t, u, v, w, x, y, z+             ]+    a = [0] ++ a + 1+    b = [0] ++ b + 1+    c = [0] ++ c + 1+    d = [0] ++ d + 1+    e = [1] ++ e + 1+    f = [1] ++ f + 1+    g = [1] ++ g + 1+    h = [1] ++ h + 1+    i = [1] ++ i + 1+    j = [1] ++ j + 1+    k = [1] ++ k + 1+    l = [1] ++ l + 1+    m = [1] ++ m + 1+{-+    n = [1] ++ n + 1+    o = [1] ++ o + 1+    p = [1] ++ p + 1+    q = [1] ++ q + 1+    r = [1] ++ r + 1+    s = [1] ++ s + 1+    t = [1] ++ t + 1+    u = [1] ++ u + 1+    v = [1] ++ v + 1+    w = [1] ++ w + 1+    x = [1] ++ x + 1+    y = [1] ++ y + 1+    z = [1] ++ z + 1+-}++verifySpec :: Verbosity -> IO ()+--verifySpec _ = interpret 30 vote+verifySpec verb = reify vote >>= verifyWithOptions defaultVerifierOptions{verbosity = verb}+                                                   mkDefaultCSettings [] "voting"

@@ -0,0 +1,194 @@+-- | This example shows an implementation of the Well-Clear Violation+-- algorithm, it follows the implementation described in 'Analysis of+-- Well-Clear Bounday Models for the Integration of UAS in the NAS',+-- https://ntrs.nasa.gov/citations/20140010078.++{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RebindableSyntax #-}++module Copilot.Verifier.Examples.ShouldPass.WCV where++import Language.Copilot+import qualified Copilot.Theorem.What4 as CT+import Copilot.Compile.C99+import Copilot.Verifier ( Verbosity, VerifierOptions(..)+                        , defaultVerifierOptions, verifyWithOptions )++import qualified Prelude as P+import Data.Foldable (forM_)+import qualified Control.Monad as Monad+++-- | `dthr` is the horizontal distance threshold.+dthr :: Stream Double+dthr = extern "dthr" Nothing++-- | `tthr` is the horizontal time threshold.+tthr :: Stream Double+tthr = extern "tthr" Nothing++-- | `zthr` is the vertical distance / altitude threshold.+zthr :: Stream Double+zthr = extern "zthr" Nothing++-- | `tcoathr` is the vertical time threshold.+tcoathr :: Stream Double+tcoathr = extern "tcoathr" Nothing++type Vect2 = (Stream Double, Stream Double)+++--------------------------------+-- External streams for relative position and velocity.+--------------------------------++-- | The relative x velocity between ownship and the intruder.+vx :: Stream Double+vx = extern "relative_velocity_x" Nothing++-- | The relative y velocity between ownship and the intruder.+vy :: Stream Double+vy = extern "relative_velocity_y" Nothing++-- | The relative z velocity between ownship and the intruder.+vz :: Stream Double+vz = extern "relative_velocity_z" Nothing++-- | The relative velocity as a 2D vector.+v :: (Stream Double, Stream Double)+v = (vx, vy)+++-- | The relative x position between ownship and the intruder.+sx :: Stream Double+sx = extern "relative_position_x" Nothing++-- | The relative y position between ownship and the intruder.+sy :: Stream Double+sy = extern "relative_position_y" Nothing++-- | The relative z position between ownship and the intruder.+sz :: Stream Double+sz = extern "relative_position_z" Nothing++-- | The relative position as a 2D vector.+s :: (Stream Double, Stream Double)+s = (sx, sy)+++------------------+-- The following section contains basic libraries for working with vectors.+------------------++-- | Multiply two Vectors.+(|*|) :: Vect2 -> Vect2 -> Stream Double+(|*|) (x1, y1) (x2, y2) = (x1 * x2) + (y1 * y2)++-- | Calculate the square of a vector.+sq :: Vect2 -> Stream Double+sq x = x |*| x++-- | Calculate the length of a vector.+norm :: Vect2 -> Stream Double+norm = sqrt . sq++-- | Calculate the determinant of two vectors.+det :: Vect2 -> Vect2 -> Stream Double+det (x1, y1) (x2, y2) = (x1 * y2) - (x2 * y1)++-- | Compare two vectors, taking into account the small error that is+-- introduced by the usage of `Double`s.+(~=) :: Stream Double -> Stream Double -> Stream Bool+a ~= b = (abs (a - b)) < 0.001++-- | Negate a vector.+neg :: Vect2 -> Vect2+neg (x, y) = (negate x, negate y)+++--------------------+-- From here on the algorithm, as described by the paper mentioned on the top+-- of this file, is implemented. Please refer to the paper for details.+--------------------++tau :: Vect2 -> Vect2 -> Stream Double+tau s v = if s |*| v < 0+            then (-(sq s)) / (s |*| v)+            else -1++tcpa :: Vect2 -> Vect2 -> Stream Double+tcpa s v@(vx, vy) = if vx ~= 0 && vy ~= 0+                      then 0+                      else -(s |*| v)/(sq v)++taumod :: Vect2 -> Vect2 -> Stream Double+taumod s v = if s |*| v < 0+               then (dthr * dthr - (sq s))/(s |*| v)+               else -1++tep :: Vect2 -> Vect2 -> Stream Double+tep s v = if (s |*| v < 0) && ((delta s v dthr) >= 0)+            then theta s v dthr (-1)+            else -1++delta :: Vect2 -> Vect2 -> Stream Double -> Stream Double+delta s v d = (d*d) * (sq v) - ((det s v)*(det s v))+-- Here the formula says : (s . orth v)^2 which is the same as det(s,v)^2++theta :: Vect2 -> Vect2 -> Stream Double -> Stream Double -> Stream Double+theta s v d e = (-(s |*| v) + e * (sqrt $ delta s v d)) / (sq v)+++tcoa :: Stream Double -> Stream Double -> Stream Double+tcoa sz vz = if (sz * vz) < 0+               then (-sz) / vz+               else -1++dcpa :: Vect2 -> Vect2 -> Stream Double+dcpa s@(sx, sy) v@(vx, vy) = norm (sx + (tcpa s v) * vx, sy + (tcpa s v) * vy)+++--------------------------+-- Well clear Violation --+--------------------------++-- | Determines if the well clear property is violated or not.+wcv :: (Vect2 -> Vect2 -> Stream Double) ->+       Vect2 -> Stream Double ->+       Vect2 -> Stream Double ->+       Stream Bool+wcv tvar s sz v vz = (horizontalWCV tvar s v) && (verticalWCV sz vz)++verticalWCV :: Stream Double -> Stream Double -> Stream Bool+verticalWCV sz vz =+  ((abs $ sz) <= zthr) ||+  (0 <= (tcoa sz vz) && (tcoa sz vz) <= tcoathr)++horizontalWCV :: (Vect2 -> Vect2 -> Stream Double) -> Vect2 -> Vect2 -> Stream Bool+horizontalWCV tvar s v =+  (norm s <= dthr) ||+  (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr))++spec = do+  Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v)))+  -- Monad.void $ prop "3d" (forAll $ (wcv tep s sz v vz)    == (wcv tep (neg s) (-sz) (neg v) (-vz)))+  trigger "well_clear_violation" (wcv tep s sz v vz) []++verifySpec :: Verbosity -> IO ()+verifySpec verb = do+  spec' <- reify spec+  verifyWithOptions defaultVerifierOptions{verbosity = verb}+                    mkDefaultCSettings [] "wcv" spec'++{-+  -- Use Z3 to prove the properties.+  results <- CT.prove CT.Z3 spec'++  -- Print the results.+  forM_ results $ \(nm, res) -> do+    putStr $ nm <> ": "+    case res of+      CT.Valid -> putStrLn "valid"+      CT.Invalid -> putStrLn "invalid"+      CT.Unknown -> putStrLn "unknown"+-}

@@ -0,0 +1,53 @@+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}+module Main (main) where++import qualified Data.CaseInsensitive as CI+import Data.CaseInsensitive (CI)+import Data.Foldable (for_)+import qualified Data.Map as Map+import qualified Data.Text as Text+import qualified Data.Text.IO as Text+import Data.Text (Text)+import Data.Traversable (for)+import Options.Applicative++import Copilot.Verifier (Verbosity(..))+import Copilot.Verifier.Examples (shouldFailExamples, shouldPassExamples)++newtype Options = Options+  { examples :: [CI Text]+  } deriving Show++optsParser :: Parser Options+optsParser = Options+  <$> (some . strArgument)+      (  metavar "EXAMPLE1 [EXAMPLE2 ...]"+      <> help "The names of the examples to run" )++main :: IO ()+main = execParser opts >>= verifyExamples+  where+    opts = info (optsParser <**> helper)+      ( fullDesc+     <> header "Run one or more copilot-verifier examples"+     <> progDesc (unlines [ "Run one or more examples from the copilot-verifier/examples directory."+                          , "Each EXAMPLE must correspond to an example name."+                          ]))++verifyExamples :: Options -> IO ()+verifyExamples Options{examples} = do+  -- Check that all requested examples exist+  examplesWithMain <- for examples $ \example ->+    case Map.lookup example (shouldFailExamples Default `Map.union` shouldPassExamples Default) of+      Just m  -> pure (example, m)+      Nothing -> fail $ "No example named " ++ Text.unpack (CI.original example)++  -- Run the examples+  for_ examplesWithMain $ \(example, exampleMain) -> do+    Text.putStrLn "====="+    Text.putStrLn $ "== Running the " <> CI.original example <> " example..."+    Text.putStrLn "====="+    Text.putStrLn ""+    exampleMain+    Text.putStrLn ""

@@ -0,0 +1,1517 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE ExplicitNamespaces #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module Copilot.Verifier+  ( verify+  , verifyWithOptions+  , VerifierOptions(..)+  , defaultVerifierOptions+  , sideCondVerifierOptions+  , Verbosity(..)+  ) where++import Control.Lens (view, (^.), to)+import Control.Monad (foldM, forM_, when)+import Control.Monad.IO.Class (liftIO)+import Control.Monad.State (execStateT, lift, StateT(..))+import Data.Aeson (ToJSON)+import Data.Foldable (traverse_)+import Data.Functor (void)+import qualified Data.Text as Text+import qualified Data.Map.Strict as Map+import Data.IORef (newIORef, modifyIORef', readIORef, IORef)+import qualified Text.LLVM.AST as L+import Data.List (genericLength)+import Data.List.NonEmpty (NonEmpty(..))+import qualified Data.List.NonEmpty as NE+import qualified Data.Vector as V+import qualified Data.BitVector.Sized as BV+import GHC.Generics (Generic)+import qualified Prettyprinter as PP+import System.Exit (exitFailure)+import System.FilePath ((</>), (<.>))++import Copilot.Compile.C99 (CSettings(..), compileWith)+import Copilot.Core+import qualified Copilot.Core.Type as CT++import qualified Copilot.Theorem.What4 as CW4++import qualified Copilot.Verifier.Log as Log++import Data.Parameterized.Ctx (EmptyCtx)+import Data.Parameterized.Context (pattern Empty)+import qualified Data.Parameterized.Context as Ctx+import Data.Parameterized.NatRepr (intValue, natValue, testEquality, knownNat, type (<=) )+import Data.Parameterized.Nonce (globalNonceGenerator)+import Data.Parameterized.Some (Some(..))+import Data.Parameterized.TraversableFC (toListFC)+import Data.Parameterized.TraversableFC.WithIndex (ifoldlMFC)+import qualified Data.Parameterized.Vector as PVec++import Lang.Crucible.Backend+  ( IsSymInterface, Goals(..), Assumptions, Assertion+  , pushAssumptionFrame, popUntilAssumptionFrame+  , getProofObligations, clearProofObligations+  , LabeledPred(..), abortExecBecause, AbortExecReason(..), addAssumption+  , addDurableProofObligation, assert, CrucibleAssumption(..), ppAbortExecReason+  , IsSymBackend(..), HasSymInterface(..)+  , labeledPred, labeledPredMsg+  -- , ProofObligations, proofGoal, goalsToList, labeledPredMsg+  )+import Lang.Crucible.Backend.Simple (newSimpleBackend)+import Lang.Crucible.CFG.Core (AnyCFG(..), cfgArgTypes, cfgReturnType)+import Lang.Crucible.CFG.Common ( freshGlobalVar )+import Lang.Crucible.FunctionHandle (newHandleAllocator)+import Lang.Crucible.Simulator+  ( SimContext(..), ctxSymInterface, ExecResult(..), ExecState(..)+  , defaultAbortHandler, runOverrideSim, partialValue, gpValue+  , GlobalVar, executeCrucible, OverrideSim, regValue+  , readGlobal, modifyGlobal, callCFG, emptyRegMap, RegEntry(..)+  , AbortedResult(..)+  )+import Lang.Crucible.Simulator.ExecutionTree ( withBackend )+import Lang.Crucible.Simulator.GlobalState ( insertGlobal )+import Lang.Crucible.Simulator.RegValue (RegValue, RegValue'(..))+import Lang.Crucible.Simulator.SimError (SimError(..), SimErrorReason(..)) -- ppSimError+import Lang.Crucible.Types+  ( TypeRepr(..), (:~:)(..), KnownRepr(..), NatType )++import Lang.Crucible.LLVM (llvmGlobals, registerLazyModule, register_llvm_overrides)+import Lang.Crucible.LLVM.Bytes (bitsToBytes)+import Lang.Crucible.LLVM.DataLayout (Alignment, DataLayout)+import Lang.Crucible.LLVM.Errors (BadBehavior)+import Lang.Crucible.LLVM.Extension (LLVM, ArchWidth)+import Lang.Crucible.LLVM.Globals (initializeAllMemory, populateAllGlobals)+import Lang.Crucible.LLVM.Intrinsics+  ( IntrinsicsOptions, OverrideTemplate, basic_llvm_override, LLVMOverride(..) )++import Lang.Crucible.LLVM.MemType+  ( MemType(..), SymType(..)+  , i1, i8, i16, i32, i64+  , memTypeSize, memTypeAlign+  , mkStructInfo+  )+import Lang.Crucible.LLVM.MemModel+  ( mkMemVar, withPtrWidth, HasLLVMAnn, LLVMAnnMap, MemImpl+  , HasPtrWidth, doResolveGlobal, doStore+  , LLVMPtr, LLVMVal, MemOptions, PartLLVMVal(..), StorageType, bitvectorType+  , ptrAdd, toStorableType, projectLLVM_bv+  , pattern LLVMPointerRepr, pattern PtrRepr, loadRaw, llvmPointer_bv+  , memRepr, Mem, unpackMemValue+  )+import Lang.Crucible.LLVM.MemModel.CallStack (CallStack)+import Lang.Crucible.LLVM.MemModel.Partial (BoolAnn(..))+import Lang.Crucible.LLVM.PrettyPrint (ppSymbol)+import Lang.Crucible.LLVM.Translation+  ( LLVMTranslationWarning(..), ModuleTranslation+  , getTranslatedCFG, translateModule, globalInitMap+  , transContext, llvmPtrWidth, llvmTypeCtx, llvmTypeAsRepr+  )+import Lang.Crucible.LLVM.TypeContext (TypeContext, llvmDataLayout)++import Crux (defaultOutputConfig)+import Crux.Config (cfgJoin, Config(..))+import Crux.Config.Load (fromFile, fromEnv)+import Crux.Config.Common+  ( cruxOptions, CruxOptions(..), postprocessOptions, outputOptions+  , OutputOptions(..)+  )+import Crux.Goal (proveGoalsOffline, provedGoalsTree)+import qualified Crux.Log as Log+import Crux.Types (SimCtxt, Crux, ProcessedGoals(..), ProofResult(..))++import Crux.LLVM.Config (llvmCruxConfig, LLVMOptions(..))+import Crux.LLVM.Compile (genBitCode)+import qualified Crux.LLVM.Log as Log+import Crux.LLVM.Simulate (setupSimCtxt, parseLLVM, explainFailure)+import CruxLLVMMain (processLLVMOptions)++import What4.Config+  (extendConfig)+import What4.Interface+  ( Pred, bvLit, bvAdd, bvUrem, bvMul, bvIsNonzero, bvEq, isEq+  , getConfiguration, freshBoundedBV, predToBV+  , getCurrentProgramLoc, printSymExpr+  , truePred, falsePred, andPred, annotateTerm, backendPred+  , getAnnotation, natAdd, natEq, natIte, natLit+  )+import What4.Expr.Builder+  ( FloatModeRepr(..), ExprBuilder, BoolExpr, startCaching+  , newExprBuilder+  )+import What4.FunctionName (functionName)+import What4.InterpretedFloatingPoint+  ( FloatInfoRepr(..), IsInterpretedFloatExprBuilder(..)+  , SingleFloat, DoubleFloat+  )+import What4.ProgramLoc (ProgramLoc, mkProgramLoc, plFunction, Position(..))+import What4.Solver.Adapter (SolverAdapter(..))+import What4.Solver.Z3 (z3Adapter)+import What4.Symbol (safeSymbol)++-- | @'verify' csettings props prefix spec@ verifies the Copilot specification+-- @spec@ under the assumptions @props@ matches the behavior of the C program+-- compiled with @csettings@ within a directory prefixed by @prefix@.+verify :: CSettings -> [String] -> String -> Spec -> IO ()+verify = verifyWithOptions defaultVerifierOptions++-- | Options for configuring the behavior of the verifier.+data VerifierOptions = VerifierOptions+  { verbosity :: Verbosity+    -- ^ How much output the verifier should produce.+  , assumePartialSideConds :: Bool+    -- ^ If 'True', the verifier will determine the conditions under which+    --   a Copilot specification's partial operations are well defined and+    --   add these side conditions as assumptions. As a result, even if the+    --   generated C code performs a partial operation, the verification will+    --   succeed if this partial operation coincides with a corresponding+    --   operation on the Copilot side.+    --+    --   If 'False', the verifier will not assume any side conditions related+    --   to partial operations in the Copilot specification. As a result, any+    --   use of a partial operation in the generated C code will cause+    --   verification to fail unless the user adds their own assumptions.+  , logSmtInteractions :: Bool+    -- ^ If 'True', create log files corresponding to the SMT solver+    -- interactions used to discharge each proof goal. The file will be named+    -- @<step>-<goal number>-<solver>.smt2@, where:+    --+    -- * @<step>@ will be either @initial-step@ or @transition-step@, depending+    --   on which step of the proof the goal corresponds to.+    --+    -- * @<goal number>@ will be the number of the goal, starting at 0 and+    --   counting up. Note that each step of the proof has its own goal+    --   numbers. This means that there can be both an+    --   @initial-step-0-<solver>.smt2@ and a @transition-step-0-<solver>.smt2@,+    --   and similarly for other numbers.+    --+    -- * @<solver>@ is the name of the SMT solver used to discharge the proof+    --   goal. Currently, this will always be @z3@, although we might make this+    --   configurable in the future.+  } deriving stock Show++-- | The default 'VerifierOptions':+--+-- * Produce a reasonable amount of diagnostics as verification proceeds+--   ('Default').+--+-- * Do not assume any side conditions related to partial operations.+--+-- * Do not log any SMT solver interactions.+defaultVerifierOptions :: VerifierOptions+defaultVerifierOptions = VerifierOptions+  { verbosity = Default+  , assumePartialSideConds = False+  , logSmtInteractions = False+  }++-- | Like 'defaultVerifierOptions', except that the verifier will assume side+-- conditions related to partial operations used in the Copilot spec.+sideCondVerifierOptions :: VerifierOptions+sideCondVerifierOptions = defaultVerifierOptions+  { assumePartialSideConds = True+  }++-- | How much output should verification produce?+--+-- The data constructors are listed in increasing order of how many diagnostics+-- they produce.+data Verbosity+  = Quiet   -- ^ Don't produce any diagnostics.+  | Default -- ^ Produce a reasonable amount of diagnostics as verification proceeds.+  | Noisy   -- ^ Produce as many diagnostics as possible.+  deriving stock (Eq, Ord, Show)++-- | Like 'verify', but with 'VerifierOptions' to more finely control the+-- verifier's behavior.+verifyWithOptions :: VerifierOptions -> CSettings -> [String] -> String -> Spec -> IO ()+verifyWithOptions opts csettings0 properties prefix spec =+  withCopilotLogging $+  do -- munge options structures into the necessary forms+     (ocfg, cruxOpts, llvmOpts, csettings, csrc) <- computeConfiguration opts csettings0 prefix+     let ?outputConfig = ocfg++     -- Compile the Copilot spec into C source code, using+     -- preexisting Copilot library calls.+     compileWith csettings prefix spec+     Log.sayCopilot $ Log.GeneratedCFile csrc++     -- Compile the C source into LLVM bitcode, using preexisting+     -- Crux library calls.+     bcFile <- genBitCode cruxOpts llvmOpts+     Log.sayCopilot $ Log.CompiledBitcodeFile prefix bcFile++     -- Run the main verification procedure+     verifyBitcode opts csettings properties spec cruxOpts llvmOpts bcFile+++-- | Do the (surprisingly large amount) of options munging necessary to set up+--   the crucible/crux environment.+computeConfiguration ::+  Log.SupportsCruxLogMessage CopilotLogging =>+  VerifierOptions -> CSettings -> FilePath ->+  IO (Log.OutputConfig CopilotLogging, CruxOptions, LLVMOptions, CSettings, FilePath)+computeConfiguration opts csettings0 prefix =+  do ocfg1 <- defaultOutputConfig copilotLoggingToSayWhat+     let quiet = verbosity opts == Quiet+     let ocfg2 mbOutputOpts = (ocfg1 mbOutputOpts) { Log._quiet = quiet }+     llvmcfg <- llvmCruxConfig+     let cfg = cfgJoin cruxOptions llvmcfg+     -- TODO, load from an actual configuration file?+     fileOpts <- fromFile "copilot-verifier" cfg Nothing+     (cruxOpts0, llvmOpts0) <- foldM fromEnv fileOpts (cfgEnv cfg)+     let odir0 = cSettingsOutputDirectory csettings0+     let odir = -- A bit grimy, but this corresponds to how crux-llvm sets+                -- its output directory.+                if odir0 == "."+                  then "results" </> prefix+                  else odir0+     let csettings = csettings0{ cSettingsOutputDirectory = odir }+     let csrc = odir </> prefix ++ ".c"+     let cruxOpts1 = cruxOpts0{ outDir = odir, bldDir = odir, inputFiles = [csrc]+                              , outputOptions =+                                  (outputOptions cruxOpts0)+                                    { quietMode = quiet+                                    , simVerbose = if verbosity opts > Default+                                                   then 2+                                                   else 0+                                    }+                              }+     let ?outputConfig = ocfg2 (Just (outputOptions cruxOpts1))+     cruxOpts2 <- postprocessOptions cruxOpts1++     -- Tweak the options passed to Clang:+     --+     -- - Fix the optimization level to -O0.+     --+     -- - Pass -ffp-contract=off to prevent sequences of floating-point+     --   multiplications/additions from being optimized to llvm.fmuladd+     --   intrinsics, which makes floating-point verification fragile.+     let llvmOpts1 = llvmOpts0+                       { optLevel = 0+                       , clangOpts = "-ffp-contract=off" : clangOpts llvmOpts0+                       }+     (cruxOpts3, llvmOpts2) <- processLLVMOptions (cruxOpts2, llvmOpts1)++     let ocfg3 = ocfg2 (Just (outputOptions cruxOpts3))+     return (ocfg3, cruxOpts3, llvmOpts2, csettings, csrc)+++data CopilotVerifierData t = CopilotVerifierData+++-- | Main entry point for the verifier.+verifyBitcode ::+  Log.Logs msgs =>+  Log.SupportsCruxLogMessage msgs =>+  Log.SupportsCruxLLVMLogMessage msgs =>+  Log.SupportsCopilotLogMessage msgs =>+  VerifierOptions {- ^ Verifier-specific settings -} ->+  CSettings   {- ^ Settings used to compile the Copilot spec. Used to find the names of functions and variables. -} ->+  [String]    {- ^ Names of properties to assume during verification. -} ->+  Spec        {- ^ The input Copilot specification -} ->+  CruxOptions {- ^ Crux options -} ->+  LLVMOptions {- ^ CruxLLVM options -} ->+  FilePath    {- ^ Path to the bitcode file to verify -} ->+  IO ()+verifyBitcode opts csettings properties spec cruxOpts llvmOpts bcFile =+  do -- Set up the expression builder and symbolic backend+     halloc <- newHandleAllocator+     sym <- newExprBuilder FloatUninterpretedRepr CopilotVerifierData globalNonceGenerator+     bak <- newSimpleBackend sym+     -- turn on hash-consing+     startCaching sym++     -- capture LLVM side-condition information for use in error reporting+     clRefs <- newCopilotLogRefs+     let ?recordLLVMAnnotation = recordLLVMAnnotation clRefs++     -- Set up the solver to use for verification.  Right now we hard-code this to Z3.+     let adapters = [z3Adapter] -- TODO? configurable+     extendConfig (solver_adapter_config_options z3Adapter) (getConfiguration sym)++     -- Set up the Crucible/LLVM simulation context+     memVar <- mkMemVar "llvm_memory" halloc+     let simctx = (setupSimCtxt halloc bak (memOpts llvmOpts) memVar)+                  { printHandle = view Log.outputHandle ?outputConfig }++     -- Load and translate the input LLVM module+     llvmMod <- parseLLVM bcFile+     Some trans <-+        let ?transOpts = transOpts llvmOpts+         in translateModule halloc memVar llvmMod++     Log.sayCopilot Log.TranslatedToCrucible++     -- Grab some metadata from the bitcode file and options;+     -- make the available via implicit arguments to the places+     -- that expect them.+     let llvmCtxt = trans ^. transContext+     let ?lc = llvmCtxt ^. llvmTypeCtx+     let ?memOpts = memOpts llvmOpts+     let ?intrinsicsOpts = intrinsicsOpts llvmOpts++     llvmPtrWidth llvmCtxt $ \ptrW ->+       withPtrWidth ptrW $++       do -- Compute the LLVM memory state with global variables allocated+          -- but not initialized+          emptyMem   <- initializeAllMemory bak llvmCtxt llvmMod++          -- Compute the LLVM memory state with global variables initialized+          -- to their initial values.+          initialMem <- populateAllGlobals bak (trans ^. globalInitMap) emptyMem++          -- Use the Copilot spec directly to compute the symbolic states+          -- necessary to carry out the states of the bisimulation proof.+          Log.sayCopilot Log.GeneratingProofState+          proofStateBundle <- CW4.computeBisimulationProofBundle sym properties spec++          -- First check that the initial state of the program matches the starting+          -- segment of the associated Copilot streams.+          let cruxOptsInit = setCruxOfflineSolverOutput "initial-step" cruxOpts+          verifyInitialState cruxOptsInit adapters clRefs simctx initialMem+             (CW4.initialStreamState proofStateBundle)++          -- Now, the real meat. Carry out the bisimulation step of the proof.+          let cruxOptsTrans = setCruxOfflineSolverOutput "transition-step" cruxOpts+          verifyStepBisimulation opts cruxOptsTrans adapters csettings+             clRefs simctx llvmMod trans memVar initialMem proofStateBundle+  where+    -- If @logSmtInteractions@ is enabled, enable offline solver output in the+    -- supplied 'CruxOptions' with the supplied file template. Otherwise, return+    -- the supplied 'CruxOptions' unaltered.+    setCruxOfflineSolverOutput :: FilePath -> CruxOptions -> CruxOptions+    setCruxOfflineSolverOutput template cruxOpts'+      | logSmtInteractions opts+      = cruxOpts'+          { offlineSolverOutput = Just $ outDir cruxOpts' </> template <.> "smt2" }+      | otherwise+      = cruxOpts'++-- | Capture LLVM side-condition information for use in error reporting.+recordLLVMAnnotation ::+  IsSymInterface sym =>+  CopilotLogRefs sym ->+  CallStack ->+  BoolAnn sym ->+  BadBehavior sym ->+  IO ()+recordLLVMAnnotation clRefs stk bann bb =+  modifyIORef' (llvmAnnMapRef clRefs) (Map.insert bann (stk, bb))++-- | Prove that the state of the global variables at program startup+--   matches the expected initial segments of the associated Copilot+--   streams.+verifyInitialState ::+  IsSymInterface sym =>+  Log.Logs msgs =>+  Log.SupportsCruxLogMessage msgs =>+  Log.SupportsCopilotLogMessage msgs =>+  sym ~ ExprBuilder t st fs =>+  HasPtrWidth wptr =>+  HasLLVMAnn sym =>+  (?memOpts :: MemOptions) =>+  (?lc :: TypeContext) =>++  CruxOptions ->+  [SolverAdapter st] ->+  CopilotLogRefs sym ->+  SimCtxt Crux sym LLVM ->+  MemImpl sym ->+  CW4.BisimulationProofState sym ->+  IO ()+verifyInitialState cruxOpts adapters clRefs simctx mem initialState =+  withBackend simctx $ \bak ->+  do Log.sayCopilot $ Log.ComputingConditions Log.InitialState+     frm <- pushAssumptionFrame bak++     assertStateRelation bak clRefs mem initialState++     popUntilAssumptionFrame bak frm++     Log.sayCopilot $ Log.ProvingConditions Log.InitialState+     proveObls cruxOpts adapters clRefs Log.InitialState simctx+++verifyStepBisimulation ::+  IsSymInterface sym =>+  Log.Logs msgs =>+  Log.SupportsCruxLogMessage msgs =>+  Log.SupportsCruxLLVMLogMessage msgs =>+  Log.SupportsCopilotLogMessage msgs =>+  sym ~ ExprBuilder t st fs =>+  HasPtrWidth wptr =>+  HasLLVMAnn sym =>+  (1 <= ArchWidth arch) =>+  HasPtrWidth (ArchWidth arch) =>+  (?memOpts :: MemOptions) =>+  (?lc :: TypeContext) =>+  (?intrinsicsOpts :: IntrinsicsOptions) =>++  VerifierOptions ->+  CruxOptions ->+  [SolverAdapter st] ->+  CSettings ->+  CopilotLogRefs sym ->+  SimCtxt Crux sym LLVM ->+  L.Module ->+  ModuleTranslation arch ->+  GlobalVar Mem ->+  MemImpl sym ->+  CW4.BisimulationProofBundle sym ->+  IO ()+verifyStepBisimulation opts cruxOpts adapters csettings clRefs simctx llvmMod modTrans memVar mem prfbundle =+  withBackend simctx $ \bak ->+  do Log.sayCopilot $ Log.ComputingConditions Log.StepBisimulation++     frm <- pushAssumptionFrame bak++     do -- set up the memory image+        mem' <- setupPrestate bak mem prfbundle++        -- sanity check, verify that we set up the memory in the expected relation+        assertStateRelation bak clRefs mem' (CW4.preStreamState prfbundle)++        -- set up trigger guard global variables+        let halloc = simHandleAllocator simctx+        -- See Note [Global variables for trigger functions]+        let prepTrigger (nm, guard, _) =+              do gv <- freshGlobalVar halloc (Text.pack (nm ++ "_called")) NatRepr+                 return (nm, gv, guard)+        triggerGlobals <- mapM prepTrigger (CW4.triggerState prfbundle)++        -- execute the step function+        let overrides = zipWith (triggerOverride clRefs) triggerGlobals (CW4.triggerState prfbundle)+        mem'' <- executeStep opts csettings clRefs simctx memVar mem' llvmMod modTrans triggerGlobals overrides (CW4.assumptions prfbundle) (CW4.sideConds prfbundle)++        -- assert the poststate is in the relation+        assertStateRelation bak clRefs mem'' (CW4.postStreamState prfbundle)++     popUntilAssumptionFrame bak frm++     Log.sayCopilot $ Log.ProvingConditions Log.StepBisimulation+     proveObls cruxOpts adapters clRefs Log.StepBisimulation simctx+++-- | Set up the "trigger override" functions.  These dummy functions+--   take the place of the external functions called by the Copilot+--   monitor when a guarded condition occurs.+--+--   Each trigger statement has a corresponding global variable that+--   is used to record if the trigger function was called; initially+--   the global is false, and is set to true when the trigger function+--   is called.  At the end of verification, we check that the value+--   of this global variable is true iff the corresponding trigger guard+--   condition is true.+--+--   The other function of the trigger overrides is to check that, when called,+--   the functions are given the expected argument values.+--+--   Otherwise, the override functions have no effects, which corresponds+--   to the assumption that the external environment makes no changes to the+--   program state that are observable to the Copilot monitor.+triggerOverride :: forall sym t arch msgs.+  IsSymInterface sym =>+  Log.Logs msgs =>+  Log.SupportsCopilotLogMessage msgs =>+  (?memOpts :: MemOptions) =>+  (?lc :: TypeContext) =>+  (?intrinsicsOpts :: IntrinsicsOptions) =>+  (1 <= ArchWidth arch) =>+  HasPtrWidth (ArchWidth arch) =>+  HasLLVMAnn sym =>++  CopilotLogRefs sym ->+  (Name, GlobalVar NatType, Pred sym) ->+  (Name, BoolExpr t, [(Some Type, CW4.XExpr sym)]) ->+  OverrideTemplate (Crux sym) sym arch (RegEntry sym Mem) EmptyCtx Mem+triggerOverride clRefs (_,triggerGlobal,_) (nm, _guard, args) =+   let args' = map toTypeRepr args in+   case Ctx.fromList args' of+     Some argCtx ->+      basic_llvm_override $+      LLVMOverride decl argCtx UnitRepr $+        \memOps bak calledArgs ->+          do let sym = backendGetSym bak+             modifyGlobal triggerGlobal $ \count -> do+               -- See Note [Global variables for trigger functions]+               countPlusOne <- liftIO $ do+                 one <- natLit sym 1+                 natAdd sym count one+               pure ((), countPlusOne)+             mem <- readGlobal memOps+             liftIO $ checkArgs bak mem (toListFC Some calledArgs) args+             return ()++ where+  decl = L.Declare+         { L.decLinkage = Nothing+         , L.decVisibility = Nothing+         , L.decRetType = L.PrimType L.Void+         , L.decName = L.Symbol nm+         , L.decArgs = map llvmArgTy args+         , L.decVarArgs = False+         , L.decAttrs = []+         , L.decComdat = Nothing+         }++  -- Use the `-CompositePtr` functions here to ensure that arguments with array+  -- or struct types are treated as pointers. See Note [Arrays and structs].+  toTypeRepr (Some ctp, _) = llvmTypeAsRepr (copilotTypeToMemTypeCompositePtr (llvmDataLayout ?lc) ctp) Some+  llvmArgTy (Some ctp, _) = copilotTypeToLLVMTypeCompositePtr ctp++  checkArgs :: forall bak. IsSymBackend sym bak =>+    bak -> MemImpl sym -> [Some (RegEntry sym)] -> [(Some Type, CW4.XExpr sym)] -> IO ()+  checkArgs bak mem = loop (0::Integer)+    where+    loop i (x:xs) ((ctp,v):vs) = checkArg bak mem i x ctp v >> loop (i+1) xs vs+    loop _ [] [] = return ()+    loop _ _ _ = fail $ "Argument list mismatch in " ++ nm++  checkArg :: forall bak. IsSymBackend sym bak =>+    bak -> MemImpl sym -> Integer -> Some (RegEntry sym) -> Some Type -> CW4.XExpr sym -> IO ()+  checkArg bak mem i (Some (RegEntry tp v)) (Some ctp) x =+    do let sym = backendGetSym bak+       eq <- computeEqualVals bak clRefs mem ctp x tp v+       (ann, eq') <- annotateTerm sym eq+       let shortmsg = "Trigger " ++ show nm ++ " argument " ++ show i+       let longmsg  = show (printSymExpr eq')+       let rsn      = AssertFailureSimError shortmsg longmsg+       loc <- getCurrentProgramLoc sym+       modifyIORef' (verifierAssertionMapRef clRefs)+         $ Map.insert (BoolAnn ann)+         $ Log.TriggerArgumentEqualityAssertion+         $ Log.SomeSome+         $ Log.TriggerArgumentEquality sym loc nm i ctp x tp v+       addDurableProofObligation bak (LabeledPred eq' (SimError loc rsn))+++-- | Actually execute the Crucible simulator on the generated "step" function.+--   This will record proof side-conditions into the symbolic backend, and+--   return the memory state corresponding to the function post-state.+--+--   This function will record side-conditions that arise from the semantics+--   of C itself (e.g., memory is accessed in bounds and signed arithmetic+--   doesn't overflow) as well as the conditions related to trigger functions.+executeStep :: forall sym arch msgs.+  IsSymInterface sym =>+  Log.Logs msgs =>+  Log.SupportsCruxLLVMLogMessage msgs =>+  Log.SupportsCopilotLogMessage msgs =>+  (?memOpts :: MemOptions) =>+  (?lc :: TypeContext) =>+  (?intrinsicsOpts :: IntrinsicsOptions) =>+  (1 <= ArchWidth arch) =>+  HasPtrWidth (ArchWidth arch) =>+  HasLLVMAnn sym =>++  VerifierOptions ->+  CSettings ->+  CopilotLogRefs sym ->+  SimCtxt Crux sym LLVM ->+  GlobalVar Mem ->+  MemImpl sym ->+  L.Module ->+  ModuleTranslation arch ->+  [(Name, GlobalVar NatType, Pred sym)] ->+  [OverrideTemplate (Crux sym) sym arch (RegEntry sym Mem) EmptyCtx Mem] ->+  [Pred sym] {- User-provided property assumptions -} ->+  [Pred sym] {- Side conditions related to partial operations -} ->+  IO (MemImpl sym)+executeStep opts csettings clRefs simctx memVar mem llvmmod modTrans triggerGlobals triggerOverrides assums sideConds =+  do globSt <- foldM setupTrigger (llvmGlobals memVar mem) triggerGlobals+     let initSt = InitialState simctx globSt defaultAbortHandler memRepr $+                    runOverrideSim memRepr runStep+     res <- executeCrucible [] initSt+     case res of+       FinishedResult _ pr -> return (pr^.partialValue.gpValue.to regValue)+       AbortedResult _ abortRes -> fail $ show $ ppAbortedResult abortRes+       TimeoutResult{} -> fail "simulation timed out!"++ where+  -- See Note [Global variables for trigger functions]+  setupTrigger gs (_,gv,_) = do+    zero <- liftIO $ natLit sym 0+    pure $ insertGlobal gv zero gs+  llvm_ctx = modTrans ^. transContext+  stepName = cSettingsStepFunctionName csettings+  sym = simctx^.ctxSymInterface++  -- TODO, would be lovely to be able to do better than dummy positions for all these things+  -- so we can correspond assumptions and asserts back to the parts of the original spec that+  -- gave rise to them.+  dummyLoc = mkProgramLoc "<>" InternalPos++  assumeProperty b =+    withBackend simctx $ \bak ->+      addAssumption bak (GenericAssumption dummyLoc "Property assumption" b)++  assumeSideCond b =+    withBackend simctx $ \bak ->+      addAssumption bak (GenericAssumption dummyLoc "Side condition for partial operation" b)++  ppAbortedResult :: AbortedResult sym ext -> PP.Doc ann+  ppAbortedResult abortRes =+    case gatherReasons abortRes of+      reason :| [] -> reason+      reasons      -> PP.vcat $ "Simulation aborted for multiple reasons."+                              : NE.toList reasons++  gatherReasons :: AbortedResult sym ext -> NonEmpty (PP.Doc ann)+  gatherReasons (AbortedExec rsn _) =+    PP.vcat ["Simulation aborted!", ppAbortExecReason rsn] :| []+  gatherReasons (AbortedExit ec) =+    PP.vcat ["Simulation called exit!", PP.viaShow ec] :| []+  gatherReasons (AbortedBranch _ _ t f) =+    gatherReasons t <> gatherReasons f++  -- Simulator entry point+  runStep :: OverrideSim (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (MemImpl sym)+  runStep =+    do -- set up built-in functions and trigger overrides+       register_llvm_overrides llvmmod [] triggerOverrides llvm_ctx+       -- set up functions defined in the module+       registerLazyModule sayTranslationWarning modTrans++       -- make any property assumptions+       liftIO (mapM_ assumeProperty assums)++       -- assume side conditions related to partial operations+       when (assumePartialSideConds opts) $ liftIO $+         mapM_ assumeSideCond sideConds++       -- look up and call the step function+       mbCfg <- liftIO $ getTranslatedCFG modTrans (L.Symbol stepName)+       () <- case mbCfg of+         Just (_, AnyCFG anyCfg, warns) -> do+           liftIO $ mapM_ sayTranslationWarning warns+           case (cfgArgTypes anyCfg, cfgReturnType anyCfg) of+             (Empty, UnitRepr) -> regValue <$> callCFG anyCfg emptyRegMap+             _ -> fail $ unwords [show stepName, "should take no arguments and return void"]+         Nothing -> fail $ unwords ["Could not find step function named", show stepName]++       -- Assert that the trigger functions were called exactly once iff the+       -- associated guard condition was true.+       -- See Note [Global variables for trigger functions].+       forM_ triggerGlobals $ \(nm, gv, guard) ->+         do expectedCount <- liftIO $ do+              one  <- natLit sym 1+              zero <- natLit sym 0+              natIte sym guard one zero+            actualCount <- readGlobal gv+            eq <- liftIO $ natEq sym expectedCount actualCount+            (ann, eq') <- liftIO $ annotateTerm sym eq+            let shortmsg = "Trigger guard equality condition: " ++ show nm+            let longmsg  = show (printSymExpr eq')+            let rsn      = AssertFailureSimError shortmsg longmsg+            liftIO+              $ modifyIORef' (verifierAssertionMapRef clRefs)+              $ Map.insert (BoolAnn ann)+              $ Log.TriggersInvokedCorrespondinglyAssertion+              $ Log.TriggersInvokedCorrespondingly dummyLoc nm expectedCount actualCount+            withBackend simctx $ \bak ->+              liftIO $ addDurableProofObligation bak (LabeledPred eq' (SimError dummyLoc rsn))++       -- return the final state of the memory+       readGlobal memVar++-- | Given a bisimulation proof bundle and an empty initial state,+--   populate the global ring-buffer variables with abstract state+--   values, and write the abstract values of the external stream+--   values into their proper locations.+setupPrestate ::+  IsSymBackend sym bak =>+  HasPtrWidth wptr =>+  HasLLVMAnn sym =>+  (?memOpts :: MemOptions) =>+  (?lc :: TypeContext) =>++  bak ->+  MemImpl sym ->+  CW4.BisimulationProofBundle sym ->+  IO (MemImpl sym)+setupPrestate bak mem0 prfbundle =+  do mem' <- foldM setupStreamState mem0 (CW4.streamState (CW4.preStreamState prfbundle))+     foldM setupExternalInput mem' (CW4.externalInputs prfbundle)++ where+   sym = backendGetSym bak++   sizeTStorage :: StorageType+   sizeTStorage = bitvectorType (bitsToBytes (intValue ?ptrWidth))++   setupExternalInput mem (nm, Some ctp, v) =+     do -- Compute LLVM/Crucible type information from the Copilot type+        let memTy      = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp+        let typeAlign  = memTypeAlign (llvmDataLayout ?lc) memTy+        stType <- toStorableType memTy+        Some typeRepr <- return (llvmTypeAsRepr memTy Some)++        -- resolve the global variable to a pointers+        ptrVal <- doResolveGlobal bak mem (L.Symbol nm)++        -- write the value into the global+        regVal <- copilotExprToRegValue sym v typeRepr+        doStore bak mem ptrVal typeRepr stType typeAlign regVal++   setupStreamState mem (nm, Some ctp, vs) =+     do -- TODO, should get these from somewhere inside copilot instead of building these names directly+        let idxName = "s" ++ show nm ++ "_idx"+        let bufName = "s" ++ show nm+        let buflen  = genericLength vs :: Integer++        -- Compute LLVM/Crucible type information from the Copilot type+        let memTy      = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp+        let typeLen    = memTypeSize (llvmDataLayout ?lc) memTy+        let typeAlign  = memTypeAlign (llvmDataLayout ?lc) memTy+        stType <- toStorableType memTy+        Some typeRepr <- return (llvmTypeAsRepr memTy Some)++        -- Resolve the global names into base pointers+        idxPtr <- doResolveGlobal bak mem (L.Symbol idxName)+        bufPtr <- doResolveGlobal bak mem (L.Symbol bufName)++        -- Create a fresh index value in the proper range+        idxVal <- freshBoundedBV sym (safeSymbol idxName) ?ptrWidth+                     (Just 0) (Just (fromIntegral (buflen - 1)))+        idxVal' <- llvmPointer_bv sym idxVal++        -- store the index value in the correct location+        let sizeTAlign = memTypeAlign (llvmDataLayout ?lc) (IntType (natValue ?ptrWidth))+        mem' <- doStore bak mem idxPtr (LLVMPointerRepr ?ptrWidth) sizeTStorage sizeTAlign idxVal'++        buflen'  <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth buflen)+        typeLen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth (toInteger typeLen))++        -- Write each value of the stream ring buffer into its correct location+        flip execStateT mem' $+          forM_ (zip vs [0 ..]) $ \(v,i) ->+            do ptrVal <- lift $+                 do x1 <- bvAdd sym idxVal =<< bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth i)+                    x2 <- bvUrem sym x1 buflen'+                    x3 <- bvMul sym x2 typeLen'+                    ptrAdd sym ?ptrWidth bufPtr x3++               regVal <- lift $ copilotExprToRegValue sym v typeRepr+               StateT $ \m ->+                 do m' <- doStore bak m ptrVal typeRepr stType typeAlign regVal+                    return ((),m')++-- | Given a memory image and a "proof state", assert that the global values+--   for each stream ring buffer have values that correspond to the given+--   stream state. This collection of assertions defines the bisimulation+--   relation.+assertStateRelation ::+  IsSymBackend sym bak =>+  Log.Logs msgs =>+  HasPtrWidth wptr =>+  HasLLVMAnn sym =>+  (?memOpts :: MemOptions) =>+  (?lc :: TypeContext) =>++  bak ->+  CopilotLogRefs sym ->+  MemImpl sym ->+  CW4.BisimulationProofState sym ->+  IO ()+assertStateRelation bak clRefs mem prfst =+  -- For each stream in the proof state, assert that the+  -- generated ring buffer global contains the corresponding+  -- values.+  forM_ (CW4.streamState prfst) assertStreamState++ where+   sym = backendGetSym bak++   sizeTStorage :: StorageType+   sizeTStorage = bitvectorType (bitsToBytes (intValue ?ptrWidth))++   assertStreamState (nm, Some ctp, vs) =+     do -- TODO, should get these from somewhere inside copilot instead of building these names directly+        let idxName = "s" ++ show nm ++ "_idx"+        let bufName = "s" ++ show nm+        let buflen  = genericLength vs :: Integer++        -- Compute LLVM/Crucible type information from the Copilot type+        let memTy      = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp+        let typeLen    = memTypeSize (llvmDataLayout ?lc) memTy+        let typeAlign  = memTypeAlign (llvmDataLayout ?lc) memTy+        stType <- toStorableType memTy+        Some typeRepr <- return (llvmTypeAsRepr memTy Some)++        -- Resolve the global names into base pointers+        idxPtr <- doResolveGlobal bak mem (L.Symbol idxName)+        bufPtr <- doResolveGlobal bak mem (L.Symbol bufName)++        -- read the value of the ring buffer index+        let sizeTAlign = memTypeAlign (llvmDataLayout ?lc) (IntType (natValue ?ptrWidth))+        (bannIdxVal, pIdxVal, idxVal) <-+          doLoadWithAnn bak mem idxPtr sizeTStorage (LLVMPointerRepr ?ptrWidth) sizeTAlign+        idxVal' <- projectLLVM_bv bak idxVal+        locIdxVal <- getCurrentProgramLoc sym+        modifyIORef' (verifierAssertionMapRef clRefs)+          $ Map.insert bannIdxVal+          $ Log.RingBufferIndexLoadAssertion+          $ Log.RingBufferIndexLoad sym locIdxVal (Text.pack idxName) pIdxVal++        buflen'  <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth buflen)+        typeLen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth (toInteger typeLen))++        -- For each value in the stream description, read a corresponding value from+        -- memory and assert that they are equal.+        forM_ (zip vs [0 ..]) $ \(v,i) ->+          do ptrVal <-+               do x1 <- bvAdd sym idxVal' =<< bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth i)+                  x2 <- bvUrem sym x1 buflen'+                  x3 <- bvMul sym x2 typeLen'+                  ptrAdd sym ?ptrWidth bufPtr x3++             (bannv', pv', v') <- doLoadWithAnn bak mem ptrVal stType typeRepr typeAlign+             locv' <- getCurrentProgramLoc sym+             let bufNameT = Text.pack bufName+             modifyIORef' (verifierAssertionMapRef clRefs)+               $ Map.insert bannv'+               $ Log.RingBufferLoadAssertion+               $ Log.SomeSome+               $ Log.RingBufferLoad sym locv' bufNameT i buflen ctp typeRepr pv'+             eq <- computeEqualVals bak clRefs mem ctp v typeRepr v'+             (ann, eq') <- annotateTerm sym eq+             let shortmsg = "State equality condition: " ++ show nm ++ " index value " ++ show i+             let longmsg  = show (printSymExpr eq')+             let rsn      = AssertFailureSimError shortmsg longmsg+             let loc      = mkProgramLoc "<>" InternalPos+             modifyIORef' (verifierAssertionMapRef clRefs)+               $ Map.insert (BoolAnn ann)+               $ Log.StreamValueEqualityAssertion+               $ Log.SomeSome+               $ Log.StreamValueEquality sym loc bufNameT i buflen ctp v typeRepr v'+             addDurableProofObligation bak (LabeledPred eq' (SimError loc rsn))++        return ()++-- | Translate the @XExpr@ values from the "Copilot.Theorem.What4" module into+--   Crucible @RegValue@s suitable for injection into the Crucible simulator.+copilotExprToRegValue :: forall sym tp.+  IsSymInterface sym =>+  sym ->+  CW4.XExpr sym ->+  TypeRepr tp ->+  IO (RegValue sym tp)+copilotExprToRegValue sym = loop+  where+    loop :: forall tp'. CW4.XExpr sym -> TypeRepr tp' -> IO (RegValue sym tp')++    loop (CW4.XBool b) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @1) =+      llvmPointer_bv sym =<< predToBV sym b knownRepr+    loop (CW4.XBool b) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @8) =+      llvmPointer_bv sym =<< predToBV sym b knownRepr+    loop (CW4.XInt8 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @8) =+      llvmPointer_bv sym x+    loop (CW4.XInt16 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @16) =+      llvmPointer_bv sym x+    loop (CW4.XInt32 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @32) =+      llvmPointer_bv sym x+    loop (CW4.XInt64 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @64) =+      llvmPointer_bv sym x+    loop (CW4.XWord8 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @8) =+      llvmPointer_bv sym x+    loop (CW4.XWord16 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @16) =+      llvmPointer_bv sym x+    loop (CW4.XWord32 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @32) =+      llvmPointer_bv sym x+    loop (CW4.XWord64 x) (LLVMPointerRepr w) | Just Refl <- testEquality w (knownNat @64) =+      llvmPointer_bv sym x++    loop (CW4.XFloat x)  (FloatRepr SingleFloatRepr) = return x+    loop (CW4.XDouble x) (FloatRepr DoubleFloatRepr) = return x++    loop CW4.XEmptyArray (VectorRepr _tpr) =+      pure V.empty+    loop (CW4.XArray xs) (VectorRepr tpr) =+      V.generateM (PVec.lengthInt xs) (\i -> loop (PVec.elemAtUnsafe i xs) tpr)+    loop (CW4.XStruct xs) (StructRepr ctx) =+      Ctx.traverseWithIndex+        (\i tpr -> RV <$> loop (xs !! Ctx.indexVal i) tpr)+        ctx++    loop x tpr =+      fail $ unlines ["Mismatch between Copilot value and crucible value", show x, show tpr]+++-- | Given an @XExpr@ from from the "Copilot.Theorem.What4" module, and+--   a Crucible @RegValue@ which is expected to match, compute an equality+--   predicate between the values.  The Crucible values may be pointers,+--   requiring us to resolve the indirection through memory; this is necessary+--   for array and struct values, but would also work for scalars.+computeEqualVals :: forall sym bak tp a wptr.+  IsSymBackend sym bak =>+  HasPtrWidth wptr =>+  HasLLVMAnn sym =>+  (?lc :: TypeContext) =>+  (?memOpts :: MemOptions) =>+  bak ->+  CopilotLogRefs sym ->+  MemImpl sym ->+  Type a ->+  CW4.XExpr sym ->+  TypeRepr tp ->+  RegValue sym tp ->+  IO (Pred sym)+computeEqualVals bak clRefs mem = loop+  where+    sym = backendGetSym bak++    loop :: forall tp' a'. Type a' -> CW4.XExpr sym -> TypeRepr tp' -> RegValue sym tp' -> IO (Pred sym)+    loop Bool (CW4.XBool b) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @1) =+      isEq sym b =<< bvIsNonzero sym =<< projectLLVM_bv bak v+    loop Bool (CW4.XBool b) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @8) =+      isEq sym b =<< bvIsNonzero sym =<< projectLLVM_bv bak v+    loop Int8 (CW4.XInt8 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @8) =+      bvEq sym x =<< projectLLVM_bv bak v+    loop Int16 (CW4.XInt16 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @16) =+      bvEq sym x =<< projectLLVM_bv bak v+    loop Int32 (CW4.XInt32 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @32) =+      bvEq sym x =<< projectLLVM_bv bak v+    loop Int64 (CW4.XInt64 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @64) =+      bvEq sym x =<< projectLLVM_bv bak v+    loop Word8 (CW4.XWord8 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @8) =+      bvEq sym x =<< projectLLVM_bv bak v+    loop Word16 (CW4.XWord16 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @16) =+      bvEq sym x =<< projectLLVM_bv bak v+    loop Word32 (CW4.XWord32 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @32) =+      bvEq sym x =<< projectLLVM_bv bak v+    loop Word64 (CW4.XWord64 x) (LLVMPointerRepr w) v | Just Refl <- testEquality w (knownNat @64) =+      bvEq sym x =<< projectLLVM_bv bak v++    loop Float (CW4.XFloat x)  (FloatRepr SingleFloatRepr) v = iFloatEq @_ @SingleFloat sym x v+    loop Double (CW4.XDouble x) (FloatRepr DoubleFloatRepr) v = iFloatEq @_ @DoubleFloat sym x v++    loop (Array _ctp) CW4.XEmptyArray (VectorRepr _tpr) vs =+      pure $ backendPred sym $ V.null vs+    loop (Array ctp) (CW4.XArray xs) (VectorRepr tpr) vs+      | PVec.lengthInt xs == V.length vs+      = V.ifoldM (\pAcc i v -> andPred sym pAcc =<< loop ctp (PVec.elemAtUnsafe i xs) tpr v)+                 (truePred sym) vs+      | otherwise+      = pure (falsePred sym)+    loop (Struct struct) (CW4.XStruct xs) (StructRepr ctx) vs+      | length copilotVals == Ctx.sizeInt (Ctx.size vs)+      = ifoldlMFC (\i pAcc tpr ->+                    case copilotVals !! Ctx.indexVal i of+                      (Value ctp _, x) ->+                        andPred sym pAcc =<< loop ctp x tpr (unRV (vs Ctx.! i)))+                  (truePred sym) ctx+      | otherwise+      = pure (falsePred sym)+      where+        copilotVals :: [(Value a', CW4.XExpr sym)]+        copilotVals = zip (toValues struct) xs++    -- If we encounter a pointer, read the memory that it points to and recurse,+    -- using the Copilot type as a guide for how much memory to read. This is+    -- needed to make array- or struct-typed arguments work (see+    -- Note [Arrays and structs]), although there is nothing about this code+    -- that is array- or struct-specific. In fact, this code could also work+    -- for pointer arguments of any other type.+    loop ctp x PtrRepr v =+      do let memTy = copilotTypeToMemTypeBool8 (llvmDataLayout ?lc) ctp+             typeAlign = memTypeAlign (llvmDataLayout ?lc) memTy+         stp <- toStorableType memTy+         llvmTypeAsRepr memTy $ \tpr ->+           do loc <- getCurrentProgramLoc sym+              (bann, p, regVal) <- doLoadWithAnn bak mem v stp tpr typeAlign+              modifyIORef' (verifierAssertionMapRef clRefs)+                $ Map.insert bann+                $ Log.PointerArgumentLoadAssertion+                $ Log.SomeSome+                $ Log.PointerArgumentLoad sym loc ctp tpr p+              loop ctp x tpr regVal++    loop _ctp x tpr _v =+      fail $ unlines ["Mismatch between Copilot value and crucible value", show x, show tpr]++-- | Convert a Copilot 'CT.Type' to a Crucible 'MemType'. 'CT.Bool's are+-- assumed to be one bit in size. See @Note [How LLVM represents bool]@.+copilotTypeToMemType ::+  DataLayout ->+  CT.Type a ->+  MemType+copilotTypeToMemType dl = loop+  where+    loop :: forall t. CT.Type t -> MemType+    loop CT.Bool   = i1+    loop CT.Int8   = i8+    loop CT.Int16  = i16+    loop CT.Int32  = i32+    loop CT.Int64  = i64+    loop CT.Word8  = i8+    loop CT.Word16 = i16+    loop CT.Word32 = i32+    loop CT.Word64 = i64+    loop CT.Float  = FloatType+    loop CT.Double = DoubleType+    loop t0@(CT.Array tp) =+      let len = fromIntegral (typeLength t0) in+      ArrayType len (copilotTypeToMemTypeBool8 dl tp)+    loop (CT.Struct v) =+      StructType (mkStructInfo dl False (map val (CT.toValues v)))++    val :: forall t. CT.Value t -> MemType+    val (CT.Value tp _) = copilotTypeToMemTypeBool8 dl tp++-- | Like 'copilotTypeToMemType', except that 'CT.Bool's are assumed to be+-- eight bits, not one bit. See @Note [How LLVM represents bool]@.+copilotTypeToMemTypeBool8 ::+  DataLayout ->+  CT.Type a ->+  MemType+copilotTypeToMemTypeBool8 _dl CT.Bool = i8+copilotTypeToMemTypeBool8 dl tp = copilotTypeToMemType dl tp++-- | Like 'copilotTypeToMemType', except that composite types (i.e.,+-- 'CT.Array's and 'CT.Struct's) are converted to 'PtrType's instead of direct+-- 'ArrayType's or 'StructType's. See @Note [Arrays and structs]@.+copilotTypeToMemTypeCompositePtr ::+  DataLayout ->+  CT.Type a ->+  MemType+copilotTypeToMemTypeCompositePtr dl (CT.Array tp) =+  PtrType (MemType (copilotTypeToMemTypeBool8 dl tp))+copilotTypeToMemTypeCompositePtr _dl (CT.Struct struct) =+  PtrType (Alias (copilotStructIdent struct))+copilotTypeToMemTypeCompositePtr dl tp = copilotTypeToMemType dl tp++-- | Convert a Copilot 'CT.Type' to an LLVM 'L.Type'. 'CT.Bool's are+-- assumed to be one bit in size. See @Note [How LLVM represents bool]@.+copilotTypeToLLVMType ::+  CT.Type a ->+  L.Type+copilotTypeToLLVMType = loop+  where+    loop :: forall t. CT.Type t -> L.Type+    loop CT.Bool   = L.PrimType (L.Integer 1)+    loop CT.Int8   = L.PrimType (L.Integer 8)+    loop CT.Int16  = L.PrimType (L.Integer 16)+    loop CT.Int32  = L.PrimType (L.Integer 32)+    loop CT.Int64  = L.PrimType (L.Integer 64)+    loop CT.Word8  = L.PrimType (L.Integer 8)+    loop CT.Word16 = L.PrimType (L.Integer 16)+    loop CT.Word32 = L.PrimType (L.Integer 32)+    loop CT.Word64 = L.PrimType (L.Integer 64)+    loop CT.Float  = L.PrimType (L.FloatType L.Float)+    loop CT.Double = L.PrimType (L.FloatType L.Double)+    loop t0@(CT.Array tp) =+      let len = fromIntegral (typeLength t0) in+      L.Array len (copilotTypeToLLVMTypeBool8 tp)+    loop (CT.Struct v) =+      -- NB: Don't use L.Struct here. That represents a literal, unnamed+      -- struct, but all of the structs used in a copilot-c99 program are+      -- named structs. As such, we must identify the struct by its alias.+      L.Alias (copilotStructIdent v)++-- | Like 'copilotTypeToLLVMType', except that 'CT.Bool's are assumed to be+-- eight bits, not one bit. See @Note [How LLVM represents bool]@.+copilotTypeToLLVMTypeBool8 ::+  CT.Type a ->+  L.Type+copilotTypeToLLVMTypeBool8 CT.Bool = L.PrimType (L.Integer 8)+copilotTypeToLLVMTypeBool8 tp = copilotTypeToLLVMType tp++-- | Like 'copilotTypeToLLVMType', except that composite types (i.e.,+-- 'CT.Array's and 'CT.Struct's) are given special treatment involving+-- pointers. See @Note [Arrays and structs]@.+copilotTypeToLLVMTypeCompositePtr ::+  CT.Type a ->+  L.Type+copilotTypeToLLVMTypeCompositePtr (CT.Array tp) =+  L.PtrTo (copilotTypeToLLVMTypeBool8 tp)+copilotTypeToLLVMTypeCompositePtr (CT.Struct struct) =+  L.PtrTo (L.Alias (copilotStructIdent struct))+copilotTypeToLLVMTypeCompositePtr tp = copilotTypeToLLVMType tp++-- | Given a struct @s@, construct the name @struct.s@ as an LLVM identifier.+copilotStructIdent :: Struct a => a -> L.Ident+copilotStructIdent struct = L.Ident $ "struct." ++ typeName struct++{-+Note [How LLVM represents bool]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+How are C values of type `bool` represented in LLVM? It depends. If it's being+stored directly a `bool`, it's represented with `i1` (i.e., a single bit). If+a `bool` is a member of some composite type, such as a pointer, array, or+struct, however, it's representing with `i8` (i.e., eight bits). This means+that we have to be careful when converting Bool-typed Copilot values, as they+can become `i1` or `i8` depending on the context.++copilot-verifier handles this by having both `copilotTypeToLLVMType` and+`copilotTypeToLLVMTypeBool8` functions. The former function treats `bool`s as+`i1`, whereas the latter treats `bool`s as `i8`. The former is used when+converting "top-level" types (e.g., the argument types in a trigger override),+whereas the latter is used when converting types that are part of a larger+composite type (e.g., the element type in an array).++The story for the `copilotTypeToMemType` and `copilotTypeToMemTypeBool8`+functions is similar.++Note [Arrays and structs]+~~~~~~~~~~~~~~~~~~~~~~~~~+When Clang compiles a function with an array argument, such as this trigger+function:++  void func(int32_t func_arg0[2]) { ... }++It will produce the following LLVM code:++  declare void @func(i32*) { ... }++Note that the argument is an i32*, not a [2 x i32]. As a result, we can't+translate Copilot array types directly to LLVM array types when they're used as+arguments to a function. This impedance mismatch is handled in two places:++1. The `copilotTypeToMemTypeCompositePtr`/`copilotTypeToLLVMTypeCompositePtr`+   functions special-case Copilot arrays such that they are translated to+   pointers. These functions are used when declaring the argument types of an+   override for a trigger function (see `triggerOverride`).+2. The `computeEqualVals` function has a special case for pointer+   arguments—see the case that matches on `PtrRepr`. When a `PtrRepr` is+   encountered, the underlying array values that it points to are read from+   memory. Because `PtrRepr` doesn't record the type of the thing being pointed+   to, `computeEqualVals` uses the corresponding Copilot type as a guide to+   determine how much memory to read and at what type the memory should be+   used. After this, `computeEqualVals` reads from the read array+   element-by-element—see the `VectorRepr` cases.++   Note that unlike `computeEqualVals`, `copilotExprToRegValue` does not need+   a `PtrRepr` case. This is because `copilotExprToRegValue` is ultimately used+   in service of calling writing elements of streams to memory, and streams do+   not store pointer values (at least, not in today's Copilot).++There is a very similar story for structs. Copilot passes structs by reference+in trigger functions (e.g., `void trigger(struct s *ss)`), so we must also load+from a `PtrRepr` in `computeEqualVals` to handle structs.++See Note [Global variables for trigger functions]+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+As part of verifying that the behavior of a Copilot specification's trigger+functions behave the same way as the trigger functions in the corresponding C+program, we check that each trigger function in the C program is invoked the+appropriate number of times. That is, if the guard condition for a trigger is+true, the C trigger function should be invoked exactly once, and if the guard+condition is false, then the trigger function should not be invoked at all.++To check this, we create a Nat-valued global variable for each trigger function+and initialize it to zero. Whenever we simulate a trigger function, we increment+the value of the corresponding global variable. At the end of simulation, we+check that the value in each global variable is equal to+`if guard_cond then 1 else 0`.+-}++-- | Like @crucible-llvm@'s @doLoad@, but also returning the 'BoolAnn' and+-- 'Pred' asserting the validity of the load.+doLoadWithAnn ::+  ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym+  , ?memOpts :: MemOptions ) =>+  bak ->+  MemImpl sym ->+  LLVMPtr sym wptr {- ^ pointer to load from      -} ->+  StorageType      {- ^ type of value to load     -} ->+  TypeRepr tp      {- ^ crucible type of the result -} ->+  Alignment        {- ^ assumed pointer alignment -} ->+  IO (BoolAnn sym, Pred sym, RegValue sym tp)+doLoadWithAnn bak mem ptr valType tpr alignment = do+    partLLVMVal <- loadRaw sym mem ptr valType alignment+    (bann, p, llvmVal) <- assertSafeWithAnn bak partLLVMVal+    regVal <- unpackMemValue sym tpr llvmVal+    pure (bann, p, regVal)+  where+    sym = backendGetSym bak++-- | Like @crucible-llvm@'s @assertSafe@, but also returning the 'BoolAnn' and+-- 'Pred' corresponding the assertion.+assertSafeWithAnn ::+  IsSymBackend sym bak =>+  bak ->+  PartLLVMVal sym ->+  IO (BoolAnn sym, Pred sym, LLVMVal sym)+assertSafeWithAnn bak partVal =+  case partVal of+    NoErr p v -> do+      (ann, p') <- annotateTerm sym p+      assert bak p' rsn+      return (BoolAnn ann, p', v)+    Err p -> do+      loc <- getCurrentProgramLoc sym+      let err = SimError loc rsn+      (_ann, p') <- annotateTerm sym p+      addProofObligation bak (LabeledPred p' err)+      abortExecBecause (AssertionFailure err)+  where+    rsn = AssertFailureSimError "Error during memory load" ""+    sym = backendGetSym bak++-- | Given a simulator state, extract any collected proof obligations,+--   attempt to prove them, and present the results to the user.+--+--   Afterward, the simulator state will be cleared of any proof obligations,+--   regardless of if they could all be proved.+proveObls ::+  IsSymInterface sym =>+  sym ~ ExprBuilder t st fs =>+  Log.Logs msgs =>+  Log.SupportsCruxLogMessage msgs =>+  Log.SupportsCopilotLogMessage msgs =>+  CruxOptions ->+  [SolverAdapter st] ->+  CopilotLogRefs sym ->+  Log.VerificationStep ->+  SimCtxt Crux sym LLVM ->+  IO ()+proveObls cruxOpts adapters clRefs step simctx =+  withBackend simctx $ \bak ->+  do let sym = backendGetSym bak+     obls <- getProofObligations bak+     clearProofObligations bak++--     mapM_ (print . ppSimError) (summarizeObls sym obls)++     vaMap <- readIORef $ verifierAssertionMapRef clRefs+     let laMapRef = llvmAnnMapRef clRefs+     laMap <- readIORef laMapRef+     results <- proveGoalsOffline adapters cruxOpts simctx (explainFailure sym laMapRef) obls+     presentResults sym vaMap laMap step results++{-+summarizeObls :: sym -> ProofObligations sym -> [SimError]+summarizeObls _ Nothing = []+summarizeObls _ (Just obls) = map (view labeledPredMsg . proofGoal) (goalsToList obls)+-}++presentResults ::+  Log.Logs msgs =>+  Log.SupportsCopilotLogMessage msgs =>+  IsSymInterface sym =>+  sym ->+  Map.Map (BoolAnn sym) (Log.VerifierAssertion sym) ->+  LLVMAnnMap sym ->+  Log.VerificationStep ->+  (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) ->+  IO ()+presentResults sym vaMap laMap step (num, goals)+  | numTotalGoals == 0+  = Log.sayCopilot Log.AllGoalsProved++    -- All goals were proven+  | numProvedGoals == numTotalGoals+  = do traverse_ (logVerifierAssertions sym vaMap laMap step num) goals+       printGoals++    -- There were some unproved goals, so fail with exit code 1+  | otherwise+  = do printGoals+       exitFailure+  where+    numTotalGoals  = totalProcessedGoals num+    numProvedGoals = provedGoals num++    printGoals =+      do Log.sayCopilot $ Log.OnlySomeGoalsProved numProvedGoals numTotalGoals+         goals' <- provedGoalsTree sym goals+         case goals' of+           Just g -> Log.logGoal g+           Nothing -> return ()++-- | Upon a successful verification, log the various assertions that the+-- verifier makes. These assertions will be visible in the output if the+-- 'verbosity' is set to 'Noisy'.+logVerifierAssertions ::+  forall sym msgs.+  IsSymInterface sym =>+  Log.Logs msgs =>+  Log.SupportsCopilotLogMessage msgs =>+  sym ->+  Map.Map (BoolAnn sym) (Log.VerifierAssertion sym) ->+  LLVMAnnMap sym ->+  Log.VerificationStep ->+  ProcessedGoals ->+  Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym) ->+  IO ()+logVerifierAssertions sym vaMap laMap step num goals = void $ go 0 goals+  where+    numTotalGoals = totalProcessedGoals num++    go :: Integer ->+          Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym) ->+          IO Integer+    go goalIdx gs =+      case gs of+        Assuming _ gs' ->+          go goalIdx gs'++        Prove (gl, locs, _) -> do+          let p = gl^.labeledPred+              nearestLoc = nearestProgramLoc locs++          -- First, obtain the verifier assertion.+          va <- case getAnnotation sym p of+            -- If the assertion has a BoolAnn, look it up in the assertion maps+            -- that we have accumulated during verification.+            Just ann+              |  Just va <- Map.lookup (BoolAnn ann) vaMap+              -> pure va+              |  Just (stk, bb) <- Map.lookup (BoolAnn ann) laMap+              -> pure $ Log.LLVMBadBehaviorCheckAssertion+                      $ Log.LLVMBadBehaviorCheck sym nearestLoc stk bb p+              |  otherwise+              -> fail $ unlines+                   [ "Cannot find BoolAnn for assertion"+                   , show $ gl^.labeledPredMsg+                   , show $ printSymExpr p+                   ]+            -- If the assertion does not have a BoolAnn, fall back to using+            -- heuristics to guess what kind of assertion it is.+            Nothing -> pure $ verifierAssertionHeuristics sym nearestLoc p++          -- Log the assertion.+          case va of+            Log.StreamValueEqualityAssertion (Log.SomeSome a) ->+              Log.sayCopilot $+              Log.StreamValueEqualityProofGoal step goalIdx numTotalGoals a+            Log.TriggersInvokedCorrespondinglyAssertion a ->+              Log.sayCopilot $+              Log.TriggersInvokedCorrespondinglyProofGoal step goalIdx numTotalGoals a+            Log.TriggerArgumentEqualityAssertion (Log.SomeSome a) ->+              Log.sayCopilot $+              Log.TriggerArgumentEqualityProofGoal step goalIdx numTotalGoals a+            Log.RingBufferLoadAssertion (Log.SomeSome a) ->+              Log.sayCopilot $+              Log.RingBufferLoadProofGoal step goalIdx numTotalGoals a+            Log.RingBufferIndexLoadAssertion a ->+              Log.sayCopilot $+              Log.RingBufferIndexLoadProofGoal step goalIdx numTotalGoals a+            Log.PointerArgumentLoadAssertion (Log.SomeSome a) ->+              Log.sayCopilot $+              Log.PointerArgumentLoadProofGoal step goalIdx numTotalGoals a+            Log.AccessorFunctionLoadAssertion a ->+              Log.sayCopilot $+              Log.AccessorFunctionLoadProofGoal step goalIdx numTotalGoals a+            Log.GuardFunctionLoadAssertion a ->+              Log.sayCopilot $+              Log.GuardFunctionLoadProofGoal step goalIdx numTotalGoals a+            Log.UnknownFunctionLoadAssertion a ->+              Log.sayCopilot $+              Log.UnknownFunctionLoadProofGoal step goalIdx numTotalGoals a+            Log.LLVMBadBehaviorCheckAssertion a ->+              Log.sayCopilot $+              Log.LLVMBadBehaviorCheckProofGoal step goalIdx numTotalGoals a++          -- Finally, return the current goal index.+          pure goalIdx++        ProveConj gs1 gs2 -> do+          goalIdx' <- go goalIdx gs1+          go (goalIdx' + 1) gs2++-- | If a verifier assertion does not have a corresponding 'BoolAnn', then we+-- must use heuristics to guess what kind of assertion it is. These heuristics+-- are not perfect, and we fall back to 'Log.UnknownFunctionLoad' in the event+-- that we cannot figure out a more obvious cause for the assertion.+verifierAssertionHeuristics ::+  IsSymInterface sym =>+  sym ->+  ProgramLoc ->+  Pred sym ->+  Log.VerifierAssertion sym+verifierAssertionHeuristics sym loc p+  | "_get" `Text.isSuffixOf` functionName funName+  = Log.AccessorFunctionLoadAssertion $+    Log.AccessorFunctionLoad sym loc funName p++  | "_guard" `Text.isSuffixOf` functionName funName+  = Log.GuardFunctionLoadAssertion $+    Log.GuardFunctionLoad sym loc funName p++  | otherwise+  = Log.UnknownFunctionLoadAssertion $+    Log.UnknownFunctionLoad sym loc funName p+  where+    funName = plFunction loc++-- | Pick the most recent 'ProgramLoc' in a trace of locations. If there are+-- no locations available, return a dummy location.+nearestProgramLoc :: [ProgramLoc] -> ProgramLoc+nearestProgramLoc locs =+  case locs of+    loc:_ -> loc+    _     -> mkProgramLoc "<>" InternalPos++-- | A collection of 'IORef's used to accumulate log messages that the verifier+-- may display at the end of verification.+data CopilotLogRefs sym = CopilotLogRefs+  { verifierAssertionMapRef :: !(IORef (Map.Map (BoolAnn sym) (Log.VerifierAssertion sym)))+    -- ^ A map of 'BoolAnn's (i.e., unique numbers) to 'Log.VerifierAssertions'.+  , llvmAnnMapRef :: !(IORef (LLVMAnnMap sym))+    -- ^ A map of 'BoolAnn's (i.e., unique numbers) to assertions about checks+    -- for bad behavior in LLVM.++    -- This is kept in a separate 'IORef' for technical reasons, as+    -- @crucible-llvm@'s 'explainFailure' function expects this 'IORef' as an+    -- argument. We could put everything into 'verifierAssertionMapRef', but+    -- that would require some tiresome 'IORef' massaging to make work.+  }++-- | Create a new 'CopilotLogRefs' value.+newCopilotLogRefs :: IsSymInterface sym => IO (CopilotLogRefs sym)+newCopilotLogRefs = do+  vaMapRef <- newIORef mempty+  laMapRef <- newIORef mempty+  pure $ CopilotLogRefs+    { verifierAssertionMapRef = vaMapRef+    , llvmAnnMapRef = laMapRef+    }++data CopilotLogging+  = LoggingCrux Log.CruxLogMessage+  | LoggingCruxLLVM Log.CruxLLVMLogMessage+  | LoggingCopilot Log.CopilotLogMessage+  deriving stock Generic+  deriving anyclass ToJSON++copilotLoggingToSayWhat :: CopilotLogging -> Log.SayWhat+copilotLoggingToSayWhat (LoggingCrux msg) = Log.cruxLogMessageToSayWhat msg+copilotLoggingToSayWhat (LoggingCruxLLVM msg) = Log.cruxLLVMLogMessageToSayWhat msg+copilotLoggingToSayWhat (LoggingCopilot msg) = Log.copilotLogMessageToSayWhat msg++withCopilotLogging ::+  ( ( Log.SupportsCruxLogMessage CopilotLogging+    , Log.SupportsCruxLLVMLogMessage CopilotLogging+    , Log.SupportsCopilotLogMessage CopilotLogging+    ) => computation ) ->+  computation+withCopilotLogging computation = do+  let ?injectCruxLogMessage = LoggingCrux+      ?injectCruxLLVMLogMessage = LoggingCruxLLVM+      ?injectCopilotLogMessage = LoggingCopilot+    in computation++sayTranslationWarning ::+  Log.Logs msgs =>+  Log.SupportsCruxLLVMLogMessage msgs =>+  LLVMTranslationWarning -> IO ()+sayTranslationWarning = Log.sayCruxLLVM . f+  where+    f (LLVMTranslationWarning s p msg) =+        Log.TranslationWarning (Text.pack (show (ppSymbol s))) (Text.pack (show p)) msg

@@ -0,0 +1,729 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ImplicitParams #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TemplateHaskell #-}+module Copilot.Verifier.Log+  ( SupportsCopilotLogMessage+  , CopilotLogMessage(..)+  , VerificationStep(..)+  , VerifierAssertion(..)+  , SomeSome(..)+  , StreamValueEquality(..)+  , TriggersInvokedCorrespondingly(..)+  , TriggerArgumentEquality(..)+  , RingBufferLoad(..)+  , RingBufferIndexLoad(..)+  , PointerArgumentLoad(..)+  , AccessorFunctionLoad(..)+  , GuardFunctionLoad(..)+  , UnknownFunctionLoad(..)+  , LLVMBadBehaviorCheck(..)+  , sayCopilot+  , copilotLogMessageToSayWhat+  ) where++import Crux (SayLevel (..), SayWhat (..))+import qualified Crux.Log as Log+import Data.Aeson (ToJSON (..), Value (..))+import Data.Aeson.TH (defaultOptions, deriveToJSON)+import Data.Kind (Type)+import qualified Data.Parameterized.Context as Ctx+import qualified Data.Parameterized.Vector as PV+import qualified Data.Parameterized.TraversableFC.WithIndex as PWI+import Data.Text (Text)+import qualified Data.Text as T+import qualified Data.Vector as V+import GHC.Generics (Generic)+import qualified Prettyprinter as PP+import qualified Prettyprinter.Render.Text as PP++import qualified Copilot.Core.Expr as CE+import qualified Copilot.Core.Type as CT+import qualified Copilot.Theorem.What4 as CW4++import qualified Lang.Crucible.Simulator as LCS+import qualified Lang.Crucible.Types as LCT+import qualified Lang.Crucible.LLVM.Errors as LCLE+import qualified Lang.Crucible.LLVM.Errors.MemoryError as LCLEME+import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as LCLEUB+import qualified Lang.Crucible.LLVM.MemModel as LCLM+import qualified Lang.Crucible.LLVM.MemModel.CallStack as LCLMCS+import qualified What4.FunctionName as WF+import qualified What4.Interface as WI+import qualified What4.ProgramLoc as WPL++data CopilotLogMessage where+  GeneratedCFile ::+       FilePath+       -- ^ The path of the generated C File+    -> CopilotLogMessage+  CompiledBitcodeFile ::+       String+       -- ^ The prefix to use in the compiled bitcode's directory+    -> FilePath+       -- ^ The name of the generated LLVM bitcode file+    -> CopilotLogMessage+  TranslatedToCrucible :: CopilotLogMessage+  GeneratingProofState :: CopilotLogMessage+  ComputingConditions :: VerificationStep -> CopilotLogMessage+  ProvingConditions :: VerificationStep -> CopilotLogMessage+  AllGoalsProved :: CopilotLogMessage+  OnlySomeGoalsProved ::+       Integer+       -- ^ Number of goals proved+    -> Integer+       -- ^ Number of total goals+    -> CopilotLogMessage++  -----+  -- Types of proof goals the verifier emits+  --+  -- The first three arguments to each constructor are:+  --+  -- * Which step of the verifier we are on+  -- * The current goal number (zero-indexed)+  -- * The total number of goals+  -----++  StreamValueEqualityProofGoal ::+       WI.IsSymExprBuilder sym+    => VerificationStep+    -> Integer+    -> Integer+    -> StreamValueEquality sym copilotType crucibleType+    -> CopilotLogMessage++  TriggersInvokedCorrespondinglyProofGoal ::+       WI.IsSymExprBuilder sym+    => VerificationStep+    -> Integer+    -> Integer+    -> TriggersInvokedCorrespondingly sym+    -> CopilotLogMessage++  TriggerArgumentEqualityProofGoal ::+       WI.IsSymExprBuilder sym+    => VerificationStep+    -> Integer+    -> Integer+    -> TriggerArgumentEquality sym copilotType crucibleType+    -> CopilotLogMessage++  RingBufferLoadProofGoal ::+       WI.IsSymExprBuilder sym+    => VerificationStep+    -> Integer+    -> Integer+    -> RingBufferLoad sym copilotType crucibleType+    -> CopilotLogMessage++  RingBufferIndexLoadProofGoal ::+       WI.IsSymExprBuilder sym+    => VerificationStep+    -> Integer+    -> Integer+    -> RingBufferIndexLoad sym+    -> CopilotLogMessage++  PointerArgumentLoadProofGoal ::+       WI.IsSymExprBuilder sym+    => VerificationStep+    -> Integer+    -> Integer+    -> PointerArgumentLoad sym copilotType crucibleType+    -> CopilotLogMessage++  AccessorFunctionLoadProofGoal ::+       WI.IsSymExprBuilder sym+    => VerificationStep+    -> Integer+    -> Integer+    -> AccessorFunctionLoad sym+    -> CopilotLogMessage++  GuardFunctionLoadProofGoal ::+       WI.IsSymExprBuilder sym+    => VerificationStep+    -> Integer+    -> Integer+    -> GuardFunctionLoad sym+    -> CopilotLogMessage++  UnknownFunctionLoadProofGoal ::+       WI.IsSymExprBuilder sym+    => VerificationStep+    -> Integer+    -> Integer+    -> UnknownFunctionLoad sym+    -> CopilotLogMessage++  LLVMBadBehaviorCheckProofGoal ::+       WI.IsSymExprBuilder sym+    => VerificationStep+    -> Integer+    -> Integer+    -> LLVMBadBehaviorCheck sym+    -> CopilotLogMessage++data VerificationStep+  = InitialState+  | StepBisimulation+  deriving stock Generic+  deriving anyclass ToJSON++-- | Types of assertions that the verifier can make, which will count towards+-- the total number of proof goals.+data VerifierAssertion sym+  = StreamValueEqualityAssertion (SomeSome (StreamValueEquality sym))+  | TriggersInvokedCorrespondinglyAssertion (TriggersInvokedCorrespondingly sym)+  | TriggerArgumentEqualityAssertion (SomeSome (TriggerArgumentEquality sym))+  | RingBufferLoadAssertion (SomeSome (RingBufferLoad sym))+  | RingBufferIndexLoadAssertion (RingBufferIndexLoad sym)+  | PointerArgumentLoadAssertion (SomeSome (PointerArgumentLoad sym))+  | AccessorFunctionLoadAssertion (AccessorFunctionLoad sym)+  | GuardFunctionLoadAssertion (GuardFunctionLoad sym)+  | UnknownFunctionLoadAssertion (UnknownFunctionLoad sym)+  | LLVMBadBehaviorCheckAssertion (LLVMBadBehaviorCheck sym)++-- | Like @Some@ in @parameterized-utils@, but existentially closing over two+-- type parameters instead of just one.+data SomeSome (f :: j -> k -> Type) where+  SomeSome :: f x y -> SomeSome f++-- | An assertion that an element in a Copilot stream is equal to the+-- corresponding element in a C ring buffer.+data StreamValueEquality sym copilotType crucibleType where+  StreamValueEquality ::+       sym+    -> WPL.ProgramLoc+       -- ^ The locations of the values+    -> Text+       -- ^ The name of the buffer+    -> Integer+       -- ^ The offset from the buffer's index, which is used to compute the+       -- element of the buffer to load+    -> Integer+       -- ^ The number of elements in the buffer+    -> CT.Type copilotType+       -- ^ The Copilot type+    -> CW4.XExpr sym+       -- ^ The Copilot value+    -> LCT.TypeRepr crucibleType+       -- ^ The Crucible type+    -> LCS.RegValue sym crucibleType+       -- ^ The Crucible value+    -> StreamValueEquality sym copilotType crucibleType++-- | An assertion that, given a Copilot trigger stream and its corresponding C+-- trigger function on a particular time step, either both fired at the same+-- time or both did not fire at all.+data TriggersInvokedCorrespondingly sym where+  TriggersInvokedCorrespondingly ::+       WPL.ProgramLoc+       -- ^ The location of the trigger+    -> CE.Name+       -- ^ The trigger name+    -> WI.SymNat sym+       -- ^ The expected number of times the trigger was fired this step+       -- (should be either 1 or 0).+    -> WI.SymNat sym+       -- ^ The actual number of times the trigger was fired this step.+    -> TriggersInvokedCorrespondingly sym++-- | An assertion that an argument to a Copilot trigger is equal to the+-- corresponding argument to a C trigger function.+data TriggerArgumentEquality sym copilotType crucibleType where+  TriggerArgumentEquality ::+       sym+    -> WPL.ProgramLoc+       -- ^ The locations of the arguments+    -> CE.Name+       -- ^ The trigger name+    -> Integer+       -- ^ The number of the argument (starting from 0)+    -> CT.Type copilotType+       -- ^ The Copilot type+    -> CW4.XExpr sym+       -- ^ The Copilot value+    -> LCT.TypeRepr crucibleType+       -- ^ The Crucible type+    -> LCS.RegValue sym crucibleType+       -- ^ The Crucible value+    -> TriggerArgumentEquality sym copilotType crucibleType++-- | An assertion that a load from a ring buffer in C is valid.+data RingBufferLoad sym copilotType crucibleType where+  RingBufferLoad ::+       sym+    -> WPL.ProgramLoc+       -- ^ The location of the trigger+    -> Text+       -- ^ The name of the buffer+    -> Integer+       -- ^ The offset from the buffer's index, which is used to compute the+       -- element of the buffer to load+    -> Integer+       -- ^ The number of elements in the buffer+    -> CT.Type copilotType+       -- ^ The Copilot type of the elements of the array+    -> LCT.TypeRepr crucibleType+       -- ^ The Crucible type of the elements of the array+    -> WI.Pred sym+       -- ^ The assertion that must hold in order for this load to be valid+    -> RingBufferLoad sym copilotType crucibleType++-- | An assertion that a load from a global variable representing a ring+-- buffer's index in C is valid.+data RingBufferIndexLoad sym where+  RingBufferIndexLoad ::+       sym+    -> WPL.ProgramLoc+       -- ^ The location of the trigger+    -> Text+       -- ^ The name of the global index+    -> WI.Pred sym+       -- ^ The assertion that must hold in order for this load to be valid+    -> RingBufferIndexLoad sym++-- | An assertion that a load from a pointer argument to a trigger function in C+-- is valid.+data PointerArgumentLoad sym copilotType crucibleType where+  PointerArgumentLoad ::+       sym+    -> WPL.ProgramLoc+       -- ^ The location of the pointer+    -> CT.Type copilotType+       -- ^ The Copilot type of the underlying memory+    -> LCT.TypeRepr crucibleType+       -- ^ The Crucible type of the underlying memory+    -> WI.Pred sym+       -- ^ The assertion that must hold in order for this load to be valid+    -> PointerArgumentLoad sym copilotType crucibleType++-- | An assertion that a load occurring from somewhere in a stream accessor+-- function in C (e.g., @s0_get@) is valid. This is a somewhat imprecise+-- assertion, as it doesn't identify /why/ the load occurs. (Most likely, it+-- happens because of an array index.)+data AccessorFunctionLoad sym where+  AccessorFunctionLoad ::+       sym+    -> WPL.ProgramLoc+       -- ^ The location of the accessor function+    -> WF.FunctionName+       -- ^ The name of the accessor function+    -> WI.Pred sym+       -- ^ The assertion that must hold in order for this load to be valid+    -> AccessorFunctionLoad sym++-- | An assertion that a load occurring from somewhere in a trigger guard+-- function in C (e.g., @even_guard@) is valid. This is a somewhat imprecise+-- assertion, as it doesn't identify /why/ the load occurs. (Most likely, it+-- happens because of an array index.)+data GuardFunctionLoad sym where+  GuardFunctionLoad ::+       sym+    -> WPL.ProgramLoc+       -- ^ The location of the guard function+    -> WF.FunctionName+       -- ^ The name of the guard function+    -> WI.Pred sym+       -- ^ The assertion that must hold in order for this load to be valid+    -> GuardFunctionLoad sym++-- | An assertion that a load occurring in some function is valid. If you+-- see this assertion, it is because the heuristics used to identify where+-- load-related assertions come from could not identify a more precise cause+-- for a load.+data UnknownFunctionLoad sym where+  UnknownFunctionLoad ::+       sym+    -> WPL.ProgramLoc+       -- ^ The location of the function+    -> WF.FunctionName+       -- ^ The name of the function+    -> WI.Pred sym+       -- ^ The assertion that must hold in order for this load to be valid+    -> UnknownFunctionLoad sym++-- | An assertion that checks that some form of bad behavior in LLVM does not+-- occur. Bad behavior includes both undefined behavior and memory unsafety.+data LLVMBadBehaviorCheck sym where+  LLVMBadBehaviorCheck ::+       sym+    -> WPL.ProgramLoc+       -- ^ The location of the check+    -> LCLMCS.CallStack+       -- ^ A call stack for the check, if one exists+    -> LCLE.BadBehavior sym+       -- ^ What type of LLVM bad behavior is being checked for+    -> WI.Pred sym+       -- ^ The assertion that must hold in order for this check to succeed+    -> LLVMBadBehaviorCheck sym++-- Silly ToJSON instances. Crux is only requiring a ToJSON constraint for+-- IDE-related functionality that we do not make use of, so the behavior of+-- these instances aren't very important.++instance ToJSON (StreamValueEquality sym copilotType crucibleType) where+  toJSON _ = String "StreamValueEquality"++instance ToJSON (TriggersInvokedCorrespondingly sym) where+  toJSON _ = String "TriggersInvokedCorrespondingly"++instance ToJSON (TriggerArgumentEquality sym copilotType crucibleType) where+  toJSON _ = String "TriggerArgumentEquality"++instance ToJSON (RingBufferLoad sym copilotType crucibleType) where+  toJSON _ = String "RingBufferLoad"++instance ToJSON (RingBufferIndexLoad sym) where+  toJSON _ = String "RingBufferIndexLoad"++instance ToJSON (PointerArgumentLoad sym copilotType crucibleType) where+  toJSON _ = String "PointerArgumentLoad"++instance ToJSON (AccessorFunctionLoad sym) where+  toJSON _ = String "AccessorFunctionLoad"++instance ToJSON (GuardFunctionLoad sym) where+  toJSON _ = String "GuardFunctionLoad"++instance ToJSON (UnknownFunctionLoad sym) where+  toJSON _ = String "UnknownFunctionLoad"++instance ToJSON (LLVMBadBehaviorCheck sym) where+  toJSON _ = String "LLVMBadBehaviorCheck"++type SupportsCopilotLogMessage msgs =+  (?injectCopilotLogMessage :: CopilotLogMessage -> msgs)++sayCopilot ::+  Log.Logs msgs =>+  SupportsCopilotLogMessage msgs =>+  CopilotLogMessage ->+  IO ()+sayCopilot msg =+  let ?injectMessage = ?injectCopilotLogMessage+   in Log.say msg++copilotTag :: Text+copilotTag = "copilot-verifier"++-- copilotFail :: Text -> SayWhat+-- copilotFail = SayWhat Fail copilotTag++copilotSimply :: Text -> SayWhat+copilotSimply = SayWhat Simply copilotTag++copilotNoisily :: Text -> SayWhat+copilotNoisily = SayWhat Noisily copilotTag++-- copilotWarn :: Text -> SayWhat+-- copilotWarn = SayWhat Warn copilotTag++copilotLogMessageToSayWhat :: CopilotLogMessage -> SayWhat+copilotLogMessageToSayWhat (GeneratedCFile csrc) =+  copilotSimply $ "Generated " <> T.pack (show csrc)+copilotLogMessageToSayWhat (CompiledBitcodeFile prefix bcFile) =+  copilotSimply $ "Compiled " <> T.pack prefix <> " into " <> T.pack bcFile+copilotLogMessageToSayWhat TranslatedToCrucible =+  copilotSimply "Translated bitcode into Crucible"+copilotLogMessageToSayWhat GeneratingProofState =+  copilotSimply "Generating proof state data"+copilotLogMessageToSayWhat (ComputingConditions step) =+  copilotSimply $ "Computing " <> describeVerificationStep step <> " verification conditions"+copilotLogMessageToSayWhat (ProvingConditions step) =+  copilotSimply $ "Proving " <> describeVerificationStep step <> " verification conditions"+copilotLogMessageToSayWhat AllGoalsProved =+  copilotSimply "All obligations proved by concrete simplification"+copilotLogMessageToSayWhat (OnlySomeGoalsProved numProvedGoals numTotalGoals) =+  copilotSimply $ T.unwords+    [ "Proved", T.pack (show numProvedGoals)+    , "of"+    , T.pack (show numTotalGoals), "total goals"+    ]+copilotLogMessageToSayWhat+    (StreamValueEqualityProofGoal step goalIdx numTotalGoals+      (StreamValueEquality+        sym loc+        bufName offset len+        copilotTy copilotVal+        crucibleTy crucibleVal)) =+  copilotNoisily $+  displayProofGoal+    step goalIdx numTotalGoals+    "asserting the equality between two stream values"+    [ renderStrict $ ppProgramLoc loc+    , "* Ring buffer name: " <> bufName+    , "* Offset into buffer (from current index): " <> T.pack (show offset)+    , "* Number of elements in buffer: " <> T.pack (show len)+    , "* Copilot type: " <> T.pack (showsCopilotType 0 copilotTy "")+    , "* Copilot value:"+    , renderStrict $ PP.indent 4 $ ppCopilotValue copilotVal+    , "* Crucible value:"+    , renderStrict $ PP.indent 4 $ ppCrucibleValue sym crucibleTy crucibleVal+    ]+copilotLogMessageToSayWhat+    (TriggersInvokedCorrespondinglyProofGoal step goalIdx numTotalGoals+      (TriggersInvokedCorrespondingly loc name expected actual)) =+  copilotNoisily $+  displayProofGoal+    step goalIdx numTotalGoals+    "asserting triggers fired in corresponding ways"+    [ renderStrict $ ppProgramLoc loc+    , "* Trigger name: " <> T.pack name+    , "* Expected number of times trigger was fired:"+    , renderStrict $ PP.indent 4 $ WI.printSymNat expected+    , "* Actual number of times trigger was fired:"+    , renderStrict $ PP.indent 4 $ WI.printSymNat actual+    ]+copilotLogMessageToSayWhat+    (TriggerArgumentEqualityProofGoal step goalIdx numTotalGoals+      (TriggerArgumentEquality+        sym loc+        triggerName argNum+        copilotTy copilotVal+        crucibleTy crucibleVal)) =+  copilotNoisily $+  displayProofGoal+    step goalIdx numTotalGoals+    "asserting the equality between two trigger arguments"+    [ renderStrict $ ppProgramLoc loc+    , "* Trigger name: " <> T.pack triggerName+    , "* Number of argument: " <> T.pack (show argNum)+    , "* Copilot type: " <> T.pack (showsCopilotType 0 copilotTy "")+    , "* Copilot value:"+    , renderStrict $ PP.indent 4 $ ppCopilotValue copilotVal+    , "* Crucible value:"+    , renderStrict $ PP.indent 4 $ ppCrucibleValue sym crucibleTy crucibleVal+    ]+copilotLogMessageToSayWhat+    (RingBufferLoadProofGoal step goalIdx numTotalGoals+      (RingBufferLoad+        _sym loc bufName offset len copilotTy _crucibleTy p)) =+  copilotNoisily $+  displayProofGoal+    step goalIdx numTotalGoals+    "asserting the validity of a memory load from a stream's ring buffer in C"+    [ renderStrict $ ppProgramLoc loc+    , "* Ring buffer name: " <> bufName+    , "* Offset into buffer (from current index): " <> T.pack (show offset)+    , "* Number of elements in buffer: " <> T.pack (show len)+    , "* Copilot type of buffer elements:" <> T.pack (showsCopilotType 0 copilotTy "")+    , "* Validity predicate:"+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p+    ]+copilotLogMessageToSayWhat+    (RingBufferIndexLoadProofGoal step goalIdx numTotalGoals+      (RingBufferIndexLoad _sym loc idxName p)) =+  copilotNoisily $+  displayProofGoal+    step goalIdx numTotalGoals+    "asserting the validity of a memory load from the index to a stream's ring buffer in C"+    [ renderStrict $ ppProgramLoc loc+    , "* Ring buffer index name: " <> idxName+    , "* Validity predicate:"+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p+    ]+copilotLogMessageToSayWhat+    (PointerArgumentLoadProofGoal step goalIdx numTotalGoals+      (PointerArgumentLoad+        _sym loc copilotTy _crucibleTy p)) =+  copilotNoisily $+  displayProofGoal+    step goalIdx numTotalGoals+    "asserting the validity of a memory load from a pointer argument to a trigger"+    [ renderStrict $ ppProgramLoc loc+    , "* Copilot type: " <> T.pack (showsCopilotType 0 copilotTy "")+    , "* Validity predicate:"+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p+    ]+copilotLogMessageToSayWhat+    (AccessorFunctionLoadProofGoal step goalIdx numTotalGoals+      (AccessorFunctionLoad _sym loc accessorName p)) =+  copilotNoisily $+  displayProofGoal+    step goalIdx numTotalGoals+    "asserting the validity of a memory load from a stream accessor function"+    [ renderStrict $ ppProgramLoc loc+    , "* Accessor function name: " <> WF.functionName accessorName+    , "* Validity predicate:"+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p+    ]+copilotLogMessageToSayWhat+    (GuardFunctionLoadProofGoal step goalIdx numTotalGoals+      (GuardFunctionLoad _sym loc accessorName p)) =+  copilotNoisily $+  displayProofGoal+    step goalIdx numTotalGoals+    "asserting the validity of a memory load from a trigger guard function"+    [ renderStrict $ ppProgramLoc loc+    , "* Guard function name: " <> WF.functionName accessorName+    , "* Validity predicate:"+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p+    ]+copilotLogMessageToSayWhat+    (UnknownFunctionLoadProofGoal step goalIdx numTotalGoals+      (UnknownFunctionLoad _sym loc accessorName p)) =+  copilotNoisily $+    displayProofGoal+    step goalIdx numTotalGoals+    "asserting the validity of a memory load from an unknown function"+    [ renderStrict $ ppProgramLoc loc+    , "* Function name: " <> WF.functionName accessorName+    , "* Validity predicate:"+    , renderStrict $ PP.indent 4 $ WI.printSymExpr p+    ]+copilotLogMessageToSayWhat+    (LLVMBadBehaviorCheckProofGoal step goalIdx numTotalGoals+      (LLVMBadBehaviorCheck _sym loc stk bb p)) =+  let ppLoc = renderStrict $ ppProgramLoc loc+      ppCallStackLines =+        [ "* Call stack:"+        , "    " <> renderCallStack stk+        ]+      ppValidPredLines =+        [ "* Validity predicate:"+        , renderStrict $ PP.indent 4 $ WI.printSymExpr p+        ] in+  case bb of+    LCLE.BBUndefinedBehavior ub ->+      copilotNoisily $+      displayProofGoal+        step goalIdx numTotalGoals+        "asserting that LLVM undefined behavior does not occur"+        $ ppLoc : ppCallStackLines +++        [ "* Undefined behavior description:"+        , renderStrict $ PP.indent 4 $ LCLEUB.ppDetails ub+        ] ++ ppValidPredLines+    LCLE.BBMemoryError me ->+      copilotNoisily $+      displayProofGoal+        step goalIdx numTotalGoals+        "asserting that LLVM memory unsafety does not occur"+        $ ppLoc : ppCallStackLines +++        [ "* Memory unsafety description:"+        , renderStrict $ PP.indent 4 $ LCLEME.explain me+        ] ++ ppValidPredLines++describeVerificationStep :: VerificationStep -> Text+describeVerificationStep InitialState     = "initial state"+describeVerificationStep StepBisimulation = "step bisimulation"++-- | Display information about an emitted proof goal.+displayProofGoal ::+     VerificationStep+  -> Integer+  -> Integer+  -> Text+  -> [Text]+  -> Text+displayProofGoal step goalIdx numTotalGoals why ls = T.unlines $+  [ banner+  , "Emitted a proof goal (" <> why <> ")"+  , "  During the " <> displayStep+  , "  Proof goal " <> T.pack (show goalIdx)+                    <> " ("+                    <> T.pack (show numTotalGoals)+                    <> " total)"+  , ""+  ]+  ++ ls ++ [banner]+  where+    banner = "====="+    displayStep =+      case step of+        InitialState ->+          "initial bisimulation state step"+        StepBisimulation ->+          "transition step of bisimulation"++ppProgramLoc :: WPL.ProgramLoc -> PP.Doc a+ppProgramLoc pl = PP.vcat+  [ "* Function:" PP.<+> PP.pretty (WPL.plFunction pl)+  , "  Position:" PP.<+> PP.pretty (WPL.plSourceLoc pl)+  ]++renderCallStack :: LCLMCS.CallStack -> Text+renderCallStack cs+  | T.null ppText+  = "<no call stack available>"+  | otherwise+  = ppText+  where+    ppText = renderStrict $ LCLMCS.ppCallStack cs++showsCopilotType :: Int -> CT.Type tp -> ShowS+showsCopilotType prec tp =+  case tp of+    CT.Bool     -> showString "Bool"+    CT.Int8     -> showString "Int8"+    CT.Int16    -> showString "Int16"+    CT.Int32    -> showString "Int32"+    CT.Int64    -> showString "Int64"+    CT.Word8    -> showString "Word8"+    CT.Word16   -> showString "Word16"+    CT.Word32   -> showString "Word32"+    CT.Word64   -> showString "Word64"+    CT.Float    -> showString "Float"+    CT.Double   -> showString "Double"+    CT.Array t  -> showParen (prec >= 11) $+                     showString "Array" .+                     showsPrec 11 (CT.typeSize tp) .+                     showsCopilotType 11 t+    CT.Struct x -> showString $ CT.typeName x++ppCopilotValue :: WI.IsSymExprBuilder sym => CW4.XExpr sym -> PP.Doc a+ppCopilotValue val =+  case val of+    CW4.XBool   b -> WI.printSymExpr b+    CW4.XInt8   i -> WI.printSymExpr i+    CW4.XInt16  i -> WI.printSymExpr i+    CW4.XInt32  i -> WI.printSymExpr i+    CW4.XInt64  i -> WI.printSymExpr i+    CW4.XWord8  w -> WI.printSymExpr w+    CW4.XWord16 w -> WI.printSymExpr w+    CW4.XWord32 w -> WI.printSymExpr w+    CW4.XWord64 w -> WI.printSymExpr w+    CW4.XFloat  f -> WI.printSymExpr f+    CW4.XDouble d -> WI.printSymExpr d+    CW4.XEmptyArray -> "[]"+    CW4.XArray  a   -> ppBracesWith ppCopilotValue (PV.toList a)+    CW4.XStruct s   -> ppBracketsWith ppCopilotValue s++ppCrucibleValue :: WI.IsSymExprBuilder sym+                => sym+                -> LCT.TypeRepr tp+                -> LCS.RegValue sym tp+                -> PP.Doc a+ppCrucibleValue sym tp val =+  case tp of+    LCLM.LLVMPointerRepr _ -> LCLM.ppPtr val+    LCT.FloatRepr _        -> WI.printSymExpr val+    LCT.VectorRepr tpr     -> ppBracketsWith (ppCrucibleValue sym tpr) (V.toList val)+    LCT.StructRepr ctx     -> withBraces $+                              PWI.itoListFC (\i (LCS.RV v) -> ppCrucibleValue sym (ctx Ctx.! i) v) val+    _ -> error $ "ppCrucibleValue: Unsupported type: " ++ show tp++renderStrict :: PP.Doc a ->  Text+renderStrict = PP.renderStrict . PP.layoutPretty PP.defaultLayoutOptions++ppBracketsWith :: (a -> PP.Doc b) -> [a] -> PP.Doc b+ppBracketsWith f = PP.align . PP.list . map f++ppBracesWith :: (a -> PP.Doc b) -> [a] -> PP.Doc b+ppBracesWith f = withBraces . map f++withBraces :: [PP.Doc a] -> PP.Doc a+withBraces =+    PP.align+  . PP.encloseSep (PP.flatAlt "{ " "{") (PP.flatAlt " }" "}") ", "++$(deriveToJSON defaultOptions ''CopilotLogMessage)

@@ -0,0 +1,32 @@+module Main (main) where++import qualified Data.CaseInsensitive as CI+import qualified Data.Map as Map+import qualified Data.Text as Text+import System.IO (stderr, stdout)+import System.IO.Silently (hSilence)+import Test.Tasty+import Test.Tasty.ExpectedFailure+import Test.Tasty.HUnit++import Copilot.Verifier (Verbosity(..))+import Copilot.Verifier.Examples (shouldFailExamples, shouldPassExamples)++main :: IO ()+main = defaultMain $+  testGroup "copilot-verifier-examples tests"+    [ testGroup "should-fail tests" $+        -- Why use hSilence for the should-fail tests when we are passing+        -- Quiet? It's because crux-llvm errors are logged at the highest+        -- severity possible, and even Crux's quietMode isn't enough to+        -- suppress those messages. We could try messing with things on the+        -- Crux side to avoid this, but it's simpler just to use hSilence here.+        -- After all, we don't really care about the output of failing tests+        -- anyway, just their exit codes.+        map (\(name, action) -> expectFail (testCase (Text.unpack (CI.original name))+                                                     (hSilence [stderr, stdout] action)))+            (Map.toAscList (shouldFailExamples Quiet))+    , testGroup "should-pass tests" $+        map (\(name, action) -> testCase (Text.unpack (CI.original name)) action)+            (Map.toAscList (shouldPassExamples Quiet))+    ]