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

[ivanperez-keera]

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]

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]

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

[RyanGlScott]

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]

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]

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]

Change Manager: Confirmed that the issue exists.