Copilot-Language/copilot

`copilot-theorem`: Crash when two externs share the same name

ivanperez-keera opened this issue · 11 comments

ivanperez-keera commented

I just ran an example where a locally defined extern was being used with multiple types, and I was met with an unexpected error message. Here's the module:

module Main where

import           Control.Monad (forM_)
import qualified Prelude       as P

import Copilot.Theorem.What4
import Language.Copilot

spec :: Spec
spec = do
  -- An example using external streams.
  let a = extern "a" Nothing
  prop "Example 7" (forAll (a || not a))

  -- An example using external streams.
  let a :: Stream Int32
      a = extern "a" Nothing
      p1 = a > 10
      p2 = a <= 10
  prop "Example 8" (forAll (p1 || p2))

  return ()

main :: IO ()
main = do
  spec' <- reify spec

  -- Use Z3 to prove the properties.
  results <- prove Z3 spec'

  -- Print the results.
  forM_ results $ \(propName, propRes) -> do
    putStr $ propName <> ": "
    case propRes of
      Valid   -> putStrLn "valid"
      Invalid -> putStrLn "invalid"
      Unknown -> putStrLn "unknown"

Here's what I was met with:

*** Exception: You have encountered a bug in Copilot/What4 translation's implementation.
*** Please create an issue at https://github.com/Copilot-Language/copilot/issues

%< --------------------------------------------------- 
  Revision:  068c06dd7ab6e900e2e8728ecb1c3b6e94ba9ccb
  Branch:    master (uncommited files present)
  Location:  Copilot.Theorem.What4
  Message:   Unexpected values in numCmp: (Ext_a > 10)
             XBool ca_a0@26:b
             XInt32 0xa:[32]
CallStack (from HasCallStack):
  panic, called at src/Copilot/Theorem/What4/Translate.hs:1504:13 in copilot-theorem-4.0-KgXuEkkLDUQ4mBFgDLT5Ib:Copilot.Theorem.What4.Translate
  panic, called at src/Copilot/Theorem/What4/Translate.hs:1128:7 in copilot-theorem-4.0-KgXuEkkLDUQ4mBFgDLT5Ib:Copilot.Theorem.What4.Translate
  unexpectedValues, called at src/Copilot/Theorem/What4/Translate.hs:1120:12 in copilot-theorem-4.0-KgXuEkkLDUQ4mBFgDLT5Ib:Copilot.Theorem.What4.Translate
%< ---------------------------------------------------

If I change the second extern definition toa = extern "b" Nothing, then the error message goes away.

This kind of error also does not manifest if both externs have the same type.

RyanGlScott commented

Interestingly, if I add a trigger or observer to the program, such as in this modified example:

module Main where

import           Control.Monad (forM_)
import qualified Prelude       as P

import Copilot.Theorem.What4
import Language.Copilot

spec :: Spec
spec = do
  -- An example using external streams.
  let a1 = extern "a" Nothing
  prop "Example 7" (forAll (a1 || not a1))

  -- An example using external streams.
  let a2 :: Stream Int32
      a2 = extern "a" Nothing
      p1 = a2 > 10
      p2 = a2 <= 10
  prop "Example 8" (forAll (p1 || p2))

  trigger "trig" (a1 || p1) []

  return ()

main :: IO ()
main = do
  spec' <- reify spec

  -- Use Z3 to prove the properties.
  results <- prove Z3 spec'

  -- Print the results.
  forM_ results $ \(propName, propRes) -> do
    putStr $ propName <> ": "
    case propRes of
      Valid   -> putStrLn "valid"
      Invalid -> putStrLn "invalid"
      Unknown -> putStrLn "unknown"

Then Copilot will reject this specification with a proper error message instead of panicking:

$ runghc Bug.hs 
Bug.hs: Copilot error: The external symbol 'a' has been declared to have two different types!
CallStack (from HasCallStack):
  error, called at src/Copilot/Language/Error.hs:24:16 in copilot-language-4.0-inplace:Copilot.Language.Error

If I comment out the trigger ... line, however, then it will panic instead. I believe the culprit is this part of Copilot's analysis functionality:

copilot/copilot-language/src/Copilot/Language/Analyze.hs

Lines 268 to 284 in 068c06d

-- | Obtain all the externs in a specification.
specExts :: IORef Env -> Spec' a -> IO ExternEnv
specExts refStreams spec = do
env <- foldM triggerExts
(ExternEnv [] [] [] [])
(triggers $ runSpec spec)
foldM observerExts env (observers $ runSpec spec)
where
observerExts :: ExternEnv -> Observer -> IO ExternEnv
observerExts env (Observer _ stream) = collectExts refStreams stream env
triggerExts :: ExternEnv -> Trigger -> IO ExternEnv
triggerExts env (Trigger _ guard args) = do
env' <- collectExts refStreams guard env
foldM (\env'' (Arg arg_) -> collectExts refStreams arg_ env'')
env' args

Notice that this collects all of the externs mentioned in the triggers or observers, but not the externs mentioned in the properties. As such, if a specification consists solely of properties (as in your original example), then this function will incorrectly conclude that the specification has no externs.

The following patch suffices to make the analysis consider externs in properties as well:

diff --git a/copilot-language/src/Copilot/Language/Analyze.hs b/copilot-language/src/Copilot/Language/Analyze.hs
index 9d326395..9acd203d 100644
--- a/copilot-language/src/Copilot/Language/Analyze.hs
+++ b/copilot-language/src/Copilot/Language/Analyze.hs
@@ -268,10 +268,13 @@ analyzeExts ExternEnv { externVarEnv  = vars
 -- | Obtain all the externs in a specification.
 specExts :: IORef Env -> Spec' a -> IO ExternEnv
 specExts refStreams spec = do
-  env <- foldM triggerExts
+  env0 <- foldM triggerExts
            (ExternEnv [] [] [] [])
            (triggers $ runSpec spec)
-  foldM observerExts env (observers $ runSpec spec)
+  env1 <- foldM observerExts
+           env0
+           (observers $ runSpec spec)
+  foldM propertyExts env1 (properties $ runSpec spec)
 
   where
   observerExts :: ExternEnv -> Observer -> IO ExternEnv
@@ -283,6 +286,9 @@ specExts refStreams spec = do
     foldM (\env'' (Arg arg_) -> collectExts refStreams arg_ env'')
           env' args
 
+  propertyExts :: ExternEnv -> Property -> IO ExternEnv
+  propertyExts env (Property _ stream) = collectExts refStreams stream env
+
 -- | Obtain all the externs in a stream.
 collectExts :: C.Typed a => IORef Env -> Stream a -> ExternEnv -> IO ExternEnv
 collectExts refStreams stream_ env_ = do

We may also want to extend the analysis to include theorems as well (the fourth type of statement that can appear in a specification besides a trigger, observer, or property).

ivanperez-keera commented

That does patch affect anything else (for example, the C code generator)?

RyanGlScott commented

I don't believe this change should affect anything besides the validity checks that Copilot performs during a call to reify. These checks don't affect the shape of the reified Copilot specification in any way, as they just reject potentially invalid programs. As such, the output of valid Copilot programs (be they C or otherwise) should remain unchanged.

ivanperez-keera commented

I think you are right. It's called during analysis, but I don't see it being called in anything that produces a result that propagates into the Copilot Core representation.

ivanperez-keera commented

Description

Copilot crashes when two externs share the same name but have different types and are used with copilot-theorem without any triggers/observers.

Type

  • Bug: exception produced when executing valid specification.

Additional context

None.

Requester

  • Ivan Perez.

Method to check presence of bug

Running the following specification, which uses two externs with the same name but different types:

module Main where

import           Control.Monad (forM_)
import qualified Prelude       as P

import Copilot.Theorem.What4
import Language.Copilot

spec :: Spec
spec = do
  -- An example using external streams.
  let a = extern "a" Nothing
  prop "Example 7" (forAll (a || not a))

  -- An example using external streams.
  let a :: Stream Int32
      a = extern "a" Nothing
      p1 = a > 10
      p2 = a <= 10
  prop "Example 8" (forAll (p1 || p2))

  return ()

main :: IO ()
main = do
  spec' <- reify spec

  -- Use Z3 to prove the properties.
  results <- prove Z3 spec'

  -- Print the results.
  forM_ results $ \(propName, propRes) -> do
    putStr $ propName <> ": "
    case propRes of
      Valid   -> putStrLn "valid"
      Invalid -> putStrLn "invalid"
      Unknown -> putStrLn "unknown"

results in a crash with the following error message:

*** Exception: You have encountered a bug in Copilot/What4 translation's implementation.
*** Please create an issue at https://github.com/Copilot-Language/copilot/issues

%< --------------------------------------------------- 
  Revision:  068c06dd7ab6e900e2e8728ecb1c3b6e94ba9ccb
  Branch:    master (uncommited files present)
  Location:  Copilot.Theorem.What4
  Message:   Unexpected values in numCmp: (Ext_a > 10)
             XBool ca_a0@26:b
             XInt32 0xa:[32]
CallStack (from HasCallStack):
  panic, called at src/Copilot/Theorem/What4/Translate.hs:1504:13 in copilot-theorem-4.0-KgXuEkkLDUQ4mBFgDLT5Ib:Copilot.Theorem.What4.Translate
  panic, called at src/Copilot/Theorem/What4/Translate.hs:1128:7 in copilot-theorem-4.0-KgXuEkkLDUQ4mBFgDLT5Ib:Copilot.Theorem.What4.Translate
  unexpectedValues, called at src/Copilot/Theorem/What4/Translate.hs:1120:12 in copilot-theorem-4.0-KgXuEkkLDUQ4mBFgDLT5Ib:Copilot.Theorem.What4.Translate
%< ---------------------------------------------------

when it should instead report the error in a graceful way.

Expected result

Copilot detects the problem and stops with a user-friendly error message.

Desired result

Copilot detects the problem and stops with a user-friendly error message.

Proposed solution

Modify the analyzer in copilot-language to also check the types of externs used in properties, so that a spec with multiple externs with inconsistent types is never let through.

Further notes

None.

ivanperez-keera commented

Change Manager: Confirmed that the issue exists.

ivanperez-keera commented

Technical Lead: Confirmed that the issue should be addressed.

ivanperez-keera commented

Technical Lead: Issue scheduled for fixing in Copilot 4.1.

Fix assigned to: @RyanGlScott .

RyanGlScott commented

Implementor: Solution implemented, review requested.

ivanperez-keera commented

Change Manager: Verified that:

  • Solution is implemented:
    • The code proposed compiles and passes all tests. Details:
      Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/272740182
    • The solution proposed produces the expected result. Details:
      Running the following Dockerfile should print a meaningful error message stating that two externs share the same name and finish gracefully (instead of printing an exception or message indicating that there is a bug in Copilot): 
      --- Dockerfile
FROM ubuntu:focal

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes libz-dev
RUN apt-get install --yes git

RUN apt-get install --yes wget
RUN mkdir -p $HOME/.ghcup/bin
RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup

RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/
RUN apt-get install --yes curl
RUN apt-get install --yes gcc g++ make libgmp3-dev
RUN apt-get install --yes pkg-config
RUN apt-get install --yes z3

SHELL ["/bin/bash", "-c"]

RUN ghcup install ghc 9.4
RUN ghcup install cabal 3.2
RUN ghcup set ghc 9.4.8
RUN cabal update

ADD TheoremNameClash.hs /tmp/TheoremNameClash.hs

CMD git clone $REPO \
    && cd $NAME \
    && git checkout $COMMIT \
    && cabal v1-sandbox init \
    && cabal v1-install alex happy --constraint='happy<2' \
    && cabal v1-install copilot**/ \
    && cabal v1-exec -- runhaskell /tmp/TheoremNameClash.hs \
    && echo Success

--- TheoremNameClash.hs
{-# LANGUAGE ScopedTypeVariables #-}   
import           Control.Monad (forM_)
import qualified Prelude       as P
import Control.Exception
import System.Exit

import Copilot.Theorem.What4
import Language.Copilot

spec :: Spec
spec = do
  -- An example using external streams.
  let a = extern "a" Nothing
  prop "Example 7" (forAll (a || not a))

  -- An example using external streams.
  let a :: Stream Int32
      a = extern "a" Nothing
      p1 = a > 10
      p2 = a <= 10
  prop "Example 8" (forAll (p1 || p2))

  return ()

main :: IO ()
main = do
  flip catch (\(e :: SomeException) -> putStrLn $ "Recovered: " P.++ displayException e) $ do
    flip catch handler $ do
      spec' <- reify spec

      -- Use Z3 to prove the properties.
      results <- prove Z3 spec'

      -- Print the results.
      forM_ results $ \(propName, propRes) -> do
        putStr $ propName <> ": "
        case propRes of
          Valid   -> putStrLn "a"
          Invalid -> putStrLn "b"
          Unknown -> putStrLn "c"
  exitSuccess
  return ()

handler :: ErrorCall -> IO ()
handler _ = putStrLn $ "You divided by 0!"
      Command (substitute variables based on new path after merge): 
      $ docker run -e "REPO=https://github.com/GaloisInc/copilot-1" -e "NAME=copilot-1" -e "COMMIT=7873c0287914b9047ff93b42373a7ac58cbc7c49" -it copilot-verify-536
  • Implementation is documented. Details:
    Internal change. No documentation needed. Auxiliary functions are short and self-explanatory.
  • Change history is clear.
  • Commit messages are clear.
  • Changelogs are updated.
  • Examples are updated. Details:
    No updates needed.
  • Required version bumps are evaluated. Details:
    No bump needed. Change is bug fix and does not affect the API.
ivanperez-keera commented

Change Manager: Implementation ready to be merged.