Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix unexpected free variable in FV #1251

Merged
merged 5 commits into from
Jul 26, 2023
Merged
Changes from 4 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
49 changes: 17 additions & 32 deletions src-tool/Pact/Analyze/Translate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,7 @@ import Data.Text (Text)
import qualified Data.Text as T
import Data.Traversable (for)
import Data.Type.Equality ((:~:) (Refl))
import Numeric.Natural (Natural)
import GHC.TypeLits (SomeSymbol(..), someSymbolVal, symbolVal)
import GHC.TypeLits hiding (SSymbol)

import qualified Pact.Types.Info as P
import Pact.Types.Lang
Expand Down Expand Up @@ -1604,10 +1603,10 @@ translateNode astNode = withAstContext astNode $ case astNode of
tsFoundVars .= []

Some tyb f' <- translateNode f
(avid, _, _) <- captureOneFreeVar
(avid, _, _) <- captureFreeVar

Some tyc g' <- translateNode g
(bvid, _, _) <- captureOneFreeVar
(bvid, _, _) <- captureFreeVar

-- important: we captured a, so we need to leave it free (by restoring
-- tsFoundVars)
Expand All @@ -1617,9 +1616,8 @@ translateNode astNode = withAstContext astNode $ case astNode of
Compose tya tyb tyc a' (Open avid "a" f') (Open bvid "b" g')

AST_NFun node SMap [ fun, l ] -> do
expectNoFreeVars
Some bTy fun' <- translateNode fun
captureOneFreeVar >>= \case
captureFreeVar >>= \case
(vid, varName, EType aType) -> translateNode l >>= \case
Some (SList listTy) l' -> do
Refl <- singEq listTy aType ?? TypeError node
Expand All @@ -1628,9 +1626,8 @@ translateNode astNode = withAstContext astNode $ case astNode of
_ -> unexpectedNode astNode

AST_NFun node SFilter [ fun, l ] -> do
expectNoFreeVars
translateNode fun >>= \case
Some SBool fun' -> captureOneFreeVar >>= \case
Some SBool fun' -> captureFreeVar >>= \case
(vid, varName, EType aType) -> translateNode l >>= \case
Some (SList listTy) l' -> do
Refl <- singEq listTy aType ?? TypeError node
Expand All @@ -1640,7 +1637,6 @@ translateNode astNode = withAstContext astNode $ case astNode of
_ -> unexpectedNode astNode

AST_NFun node SFold [ fun, a, l ] -> do
expectNoFreeVars
Some funTy fun' <- translateNode fun

-- Note: The order of these variables is important. `a` should be the first
Expand All @@ -1651,8 +1647,8 @@ translateNode astNode = withAstContext astNode $ case astNode of
--
-- `a` encountered first, `b` will be consed on top of it, resulting in the
-- variables coming out backwards.
captureTwoFreeVars >>= \case
[ (vidb, varNameb, EType tyb), (vida, varNamea, EType tya) ] -> do
liftM2 (,) captureFreeVar captureFreeVar >>= \case
((vidb, varNameb, EType tyb), (vida, varNamea, EType tya)) -> do
Some aTy' a' <- translateNode a
translateNode l >>= \case
Some (SList listTy) l' -> do
Expand All @@ -1662,17 +1658,15 @@ translateNode astNode = withAstContext astNode $ case astNode of
pure $ Some tya $ CoreTerm $
ListFold tya tyb (Open vida varNamea (Open vidb varNameb fun')) a' l'
_ -> unexpectedNode astNode
_ -> unexpectedNode astNode

AST_NFun _ name [ f, g, a ]
| name == SAndQ || name == SOrQ -> do
expectNoFreeVars
translateNode f >>= \case
Some SBool f' -> do
(fvid, fvarName, _) <- captureOneFreeVar
(fvid, fvarName, _) <- captureFreeVar
translateNode g >>= \case
Some SBool g' -> do
(gvid, gvarName, _) <- captureOneFreeVar
(gvid, gvarName, _) <- captureFreeVar
Some aTy' a' <- translateNode a
pure $ Some SBool $ CoreTerm $ (if name == "and?" then AndQ else OrQ)
aTy' (Open fvid fvarName f') (Open gvid gvarName g') a'
Expand All @@ -1681,9 +1675,8 @@ translateNode astNode = withAstContext astNode $ case astNode of

AST_NFun _ SWhere [ field, fun, obj ] -> translateNode field >>= \case
Some SStr field' -> do
expectNoFreeVars
translateNode fun >>= \case
Some SBool fun' -> captureOneFreeVar >>= \case
Some SBool fun' -> captureFreeVar >>= \case
(vid, varName, EType freeTy) -> translateNode obj >>= \case
Some objTy@SObject{} obj' -> pure $ Some SBool $ CoreTerm $
Where objTy freeTy field' (Open vid varName fun') obj'
Expand Down Expand Up @@ -1848,23 +1841,14 @@ trackCapScope capName act = do
tsStaticCapsInScope .= current
return r

captureOneFreeVar :: TranslateM (VarId, Text, EType)
captureOneFreeVar = do
vs <- use tsFoundVars
tsFoundVars .= []
case vs of
[v] -> pure v
_ -> throwError' $ FreeVarInvariantViolation $
"unexpected vars found: " <> tShow vs

captureTwoFreeVars :: TranslateM [(VarId, Text, EType)]
captureTwoFreeVars = do
captureFreeVar :: TranslateM (VarId, Text, EType)
captureFreeVar = do
vs <- use tsFoundVars
tsFoundVars .= []
case vs of
[_, _] -> pure vs
_ -> throwError' $ FreeVarInvariantViolation $
"unexpected vars found: " <> tShow vs
v:vs' -> do
tsFoundVars .= vs'
pure v
_ -> throwError' $ FreeVarInvariantViolation "expected var"

expectNoFreeVars :: TranslateM ()
expectNoFreeVars = do
Expand Down Expand Up @@ -1938,6 +1922,7 @@ runTranslation modName funName info caps pactArgs body checkType = do
CheckDefconst
-> error "invariant violation: this cannot be a constant"
_ <- extendPath -- form final edge for any remaining events
expectNoFreeVars
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

final check that no free vars are dangling

pure res

handleState translateState =
Expand Down