local streams can escape their lexical scope

The local combinator is intended to act like an internal let operation, but doesn't seem to be handled correctly. In particular, if a stream bound via local is passed into an operator that uses Drop or Append, the resulting local variable will be referred to out of context. This is basically because code consuming core Stream definitions expects the stream recurrence expression not to have any free variables, but this is not guaranteed by reification. In contrast, an ordinary Haskell let has the desired behavior.

This can be seen in both the stream interpreter and in the code generator. Consider the following spec:

-- External temperature as a byte in degrees C
temp :: Stream Word8
temp = extern "temperature" (Just [1 .. 100])

-- width of the sliding window
window :: Int
window = 3

-- Compute a sum of the last 3 samples
sumTemp :: Stream Word32
sumTemp = local (cast temp) $ \t -> sum window (replicate 3 19 ++ t)

spec :: Spec
spec = do
  trigger "heaton"  (sumTemp < (18*fromIntegral window)) [arg sumTemp]
  trigger "heatoff" (sumTemp > (21*fromIntegral window)) [arg sumTemp]

When interpreted, this yields:

Maybe.fromJust: Nothing
CallStack (from HasCallStack):
  error, called at libraries/base/Data/Maybe.hs:148:21 in base:Data.Maybe
  fromJust, called at src/Copilot/Core/Interpret/Eval.hs:156:41 in copilot-core-3.5-inplace:Copilot.Core.Interpret.Eval

When used for code generation, this yields code which, when compiled, causes:

heater.c:36:10: error: use of undeclared identifier 'local_0'
  return local_0;
         ^
heater.c:40:10: error: use of undeclared identifier 'local_2'
  return local_2;
         ^
heater.c:44:10: error: use of undeclared identifier 'local_4'
  return local_4;
         ^
heater.c:48:10: error: use of undeclared identifier 'local_6'
  return local_6;

I think that if the reification of all expressions was memoized using makeDynStableName, the same way that streams already are, you'd get better results on existing specs and also remove the need for local altogether (i.e., you could just use let instead).

Add support for `local`, `var` and `label` expressions in the What4 m…

@robdockins

@robdockins Just keeping you in the loop.

We had a quick discussion about this today. This looks like a proper bug and should take priority. We probably won't be able to fix it before the very next release (3.6), but we'll try to address it by the following one.

Add support for `local`, `var` and `label` expressions in the What4 m…

Description

C99 backend generates incorrect code when local is used with a delay (append). The generated code uses variables that are not defined in the same scope.

Type

Bug: generated C code is incorrect, uses undefined variable.

Additional context

None.

Requester

Rob Dockins (Galois)

Method to check presence of bug

Given this Copilot spec:

{-# LANGUAGE CPP #-}
module Main where

import qualified Prelude as P

import Language.Copilot hiding (interpret)

#ifdef COMPILE
import Copilot.Compile.C99
#else
import Copilot.Interpret
#endif

delayed :: Stream Word8
delayed = local (constW8 1) $ \t -> [0] ++ t

spec :: Spec
spec =
  trigger "on" (delayed < 10) [arg delayed]

main :: IO ()
main = do
  spec' <- reify spec
#ifdef COMPILE
  compile "local" spec'
#else
  putStrLn (interpret Table 10 spec')
#endif

Running or compiling that code results in errors both using the interpreter and the C99 backend:

$ cabal v1-exec -- runhaskell Local.hs                # With the interpreter
Local.hs: Maybe.fromJust: Nothing

$ cabal v1-exec -- runhaskell -DCOMPILE Local.hs && gcc -c local.c       # With the C99 backend
local.c: In function ‘s1_gen’:
local.c:24:10: error: ‘local_0’ undeclared (first use in this function); did you mean ‘locale_t’?
   24 |   return local_0;
      |          ^~~~~~~
      |          locale_t
local.c:24:10: note: each undeclared identifier is reported only once for each function it appears in
local.c: In function ‘s3_gen’:
local.c:28:10: error: ‘local_2’ undeclared (first use in this function); did you mean ‘locale_t’?
   28 |   return local_2;
      |          ^~~~~~~
      |          locale_t

Expected result

The executions above should execute without failures. The interpreter should produce no output.

Desired result

The executions above should execute without failures. The interpreter should produce no output.

Proposed solution

To be determined.

Further notes

None.

Change Manager: Confirmed that the issue exists.

Technical Lead: Confirmed that the issue should be addressed.

Navigation Menu

Repository navigation

`local` streams can escape their lexical scope #253

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

local streams can escape their lexical scope #253

Description

Activity

robdockins commented on Sep 17, 2021

ivanperez-keera commented on Oct 1, 2021

ivanperez-keera commented on Aug 15, 2023

ivanperez-keera commented on Aug 15, 2023

ivanperez-keera commented on Aug 15, 2023

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

`local` streams can escape their lexical scope #253