From 7d0ed3c89d7efb7ef55710d04ffba0a9de4627e6 Mon Sep 17 00:00:00 2001 From: strikef Date: Fri, 14 Mar 2025 11:26:15 +0900 Subject: [PATCH 1/5] throw `DropIndexOverflow` only when drop length exceeds app length --- copilot-language/src/Copilot/Language/Analyze.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-language/src/Copilot/Language/Analyze.hs b/copilot-language/src/Copilot/Language/Analyze.hs index e7065f7b4..1b72c9aed 100644 --- a/copilot-language/src/Copilot/Language/Analyze.hs +++ b/copilot-language/src/Copilot/Language/Analyze.hs @@ -188,7 +188,7 @@ analyzeAppend refStreams dstn e b f = do -- append. analyzeDrop :: Int -> Stream a -> IO () analyzeDrop k (Append xs _ _) - | k >= length xs = throw DropIndexOverflow + | k > length xs = throw DropIndexOverflow | k > fromIntegral (maxBound :: DropIdx) = throw DropMaxViolation | otherwise = return () analyzeDrop _ _ = throw DropAppliedToNonAppend From 9e393183a78e055454cdf8c21d452f7b6d83363d Mon Sep 17 00:00:00 2001 From: strikef Date: Fri, 14 Mar 2025 11:27:24 +0900 Subject: [PATCH 2/5] simplify `drop k (app k s)` to avoid erroneous C codegen when |drop| == |app| --- copilot-language/src/Copilot/Language/Reify.hs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/copilot-language/src/Copilot/Language/Reify.hs b/copilot-language/src/Copilot/Language/Reify.hs index 60bae450b..2a9f5379b 100644 --- a/copilot-language/src/Copilot/Language/Reify.hs +++ b/copilot-language/src/Copilot/Language/Reify.hs @@ -147,9 +147,12 @@ mkExpr refMkId refStreams refMap = go ------------------------------------------------------ Drop k e1 -> case e1 of - Append _ _ _ -> do - s <- mkStream refMkId refStreams refMap e1 - return $ Core.Drop typeOf (fromIntegral k) s + Append a _ s -> + if k == length a + then go s + else do + _s <- mkStream refMkId refStreams refMap e1 + return $ Core.Drop typeOf (fromIntegral k) _s _ -> impossible "mkExpr" "copilot-language" ------------------------------------------------------ From 67482fce9c146346a4ee69433b20cce191f3ed38 Mon Sep 17 00:00:00 2001 From: strikef Date: Thu, 27 Mar 2025 14:51:02 +0900 Subject: [PATCH 3/5] Move fix to `Temporal` and add explanatory comments --- .../src/Copilot/Language/Operators/Temporal.hs | 16 +++++++++------- copilot-language/src/Copilot/Language/Reify.hs | 9 +++------ 2 files changed, 12 insertions(+), 13 deletions(-) diff --git a/copilot-language/src/Copilot/Language/Operators/Temporal.hs b/copilot-language/src/Copilot/Language/Operators/Temporal.hs index 37b0d9a22..49fc1be6d 100644 --- a/copilot-language/src/Copilot/Language/Operators/Temporal.hs +++ b/copilot-language/src/Copilot/Language/Operators/Temporal.hs @@ -1,5 +1,4 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. - {-# LANGUAGE Safe #-} -- | Temporal stream transformations. @@ -11,7 +10,7 @@ module Copilot.Language.Operators.Temporal import Copilot.Core (Typed) import Copilot.Language.Prelude import Copilot.Language.Stream -import Prelude () +import Prelude ((==)) infixr 1 ++ @@ -32,8 +31,11 @@ infixr 1 ++ -- elements. For most kinds of streams, you cannot drop elements without -- prepending an equal or greater number of elements to them first, as it -- could result in undefined samples. -drop :: Typed a => Int -> Stream a -> Stream a -drop 0 s = s -drop _ ( Const j ) = Const j -drop i ( Drop j s ) = Drop (fromIntegral i + j) s -drop i s = Drop (fromIntegral i) s +drop :: (Typed a) => Int -> Stream a -> Stream a +drop 0 s = s +-- Along with simplifying the Stream, this also avoids the invalid C code +-- generated from append (array) and drop (indexing) when their lengths are the same +drop i (Append a _ s) | i == length a = s +drop _ (Const j) = Const j +drop i (Drop j s) = Drop (fromIntegral i + j) s +drop i s = Drop (fromIntegral i) s diff --git a/copilot-language/src/Copilot/Language/Reify.hs b/copilot-language/src/Copilot/Language/Reify.hs index 2a9f5379b..a0256c3b2 100644 --- a/copilot-language/src/Copilot/Language/Reify.hs +++ b/copilot-language/src/Copilot/Language/Reify.hs @@ -147,12 +147,9 @@ mkExpr refMkId refStreams refMap = go ------------------------------------------------------ Drop k e1 -> case e1 of - Append a _ s -> - if k == length a - then go s - else do - _s <- mkStream refMkId refStreams refMap e1 - return $ Core.Drop typeOf (fromIntegral k) _s + Append _ _ _ -> do + s <- mkStream refMkId refStreams refMap e1 + return $ Core.Drop typeOf (fromIntegral k) s _ -> impossible "mkExpr" "copilot-language" ------------------------------------------------------ From b1ad2288cccd8d71e84d477bfd625e93625dbb3f Mon Sep 17 00:00:00 2001 From: strikef Date: Thu, 27 Mar 2025 14:55:24 +0900 Subject: [PATCH 4/5] Remove redundant diff --- copilot-language/src/Copilot/Language/Reify.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-language/src/Copilot/Language/Reify.hs b/copilot-language/src/Copilot/Language/Reify.hs index a0256c3b2..60bae450b 100644 --- a/copilot-language/src/Copilot/Language/Reify.hs +++ b/copilot-language/src/Copilot/Language/Reify.hs @@ -148,8 +148,8 @@ mkExpr refMkId refStreams refMap = go Drop k e1 -> case e1 of Append _ _ _ -> do - s <- mkStream refMkId refStreams refMap e1 - return $ Core.Drop typeOf (fromIntegral k) s + s <- mkStream refMkId refStreams refMap e1 + return $ Core.Drop typeOf (fromIntegral k) s _ -> impossible "mkExpr" "copilot-language" ------------------------------------------------------ From c6e7a9943e3caadae5811420a79ce9e0e88b432a Mon Sep 17 00:00:00 2001 From: strikef Date: Thu, 27 Mar 2025 15:00:06 +0900 Subject: [PATCH 5/5] Fix indent and formatting --- .../src/Copilot/Language/Operators/Temporal.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/copilot-language/src/Copilot/Language/Operators/Temporal.hs b/copilot-language/src/Copilot/Language/Operators/Temporal.hs index 49fc1be6d..45ce5c119 100644 --- a/copilot-language/src/Copilot/Language/Operators/Temporal.hs +++ b/copilot-language/src/Copilot/Language/Operators/Temporal.hs @@ -32,10 +32,10 @@ infixr 1 ++ -- prepending an equal or greater number of elements to them first, as it -- could result in undefined samples. drop :: (Typed a) => Int -> Stream a -> Stream a -drop 0 s = s +drop 0 s = s -- Along with simplifying the Stream, this also avoids the invalid C code -- generated from append (array) and drop (indexing) when their lengths are the same -drop i (Append a _ s) | i == length a = s -drop _ (Const j) = Const j -drop i (Drop j s) = Drop (fromIntegral i + j) s -drop i s = Drop (fromIntegral i) s +drop i ( Append a _ s ) | i == length a = s +drop _ ( Const j ) = Const j +drop i ( Drop j s ) = Drop (fromIntegral i + j) s +drop i s = Drop (fromIntegral i) s