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

Fill out more scheme builtins #4355

Merged
merged 16 commits into from
Oct 25, 2023
Merged
Show file tree
Hide file tree
Changes from all 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
6 changes: 6 additions & 0 deletions parser-typechecker/src/Unison/Builtin.hs
Original file line number Diff line number Diff line change
Expand Up @@ -833,6 +833,12 @@ ioBuiltins =
( "validateSandboxed",
forall1 "a" $ \a -> list termLink --> a --> boolean
),
("sandboxLinks", termLink --> io (list termLink)),
( "Value.validateSandboxed",
list termLink
--> value
--> io (eithert (list termLink) (list termLink))
),
("Tls.newClient.impl.v3", tlsClientConfig --> socket --> iof tls),
("Tls.newServer.impl.v3", tlsServerConfig --> socket --> iof tls),
("Tls.handshake.impl.v3", tls --> iof unit),
Expand Down
2 changes: 2 additions & 0 deletions parser-typechecker/src/Unison/Runtime/ANF.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1416,6 +1416,8 @@ data POp
| -- STM
ATOM
| TFRC -- try force
| SDBL -- sandbox link list
| SDBV -- sandbox check for Values
deriving (Show, Eq, Ord, Enum, Bounded)

type ANormal = ABTN.Term ANormalF
Expand Down
4 changes: 3 additions & 1 deletion parser-typechecker/src/Unison/Runtime/ANF/Serialize.hs
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@ import Data.Word (Word16, Word32, Word64)
import GHC.Stack
import Unison.ABT.Normalized (Term (..))
import Unison.Reference (Reference, Reference' (Builtin), pattern Derived)
import Unison.Runtime.Array qualified as PA
import Unison.Runtime.ANF as ANF hiding (Tag)
import Unison.Runtime.Array qualified as PA
import Unison.Runtime.Exception
import Unison.Runtime.Serialize
import Unison.Util.EnumContainers qualified as EC
Expand Down Expand Up @@ -618,6 +618,8 @@ pOpCode op = case op of
DBTX -> 119
IXOT -> 120
IXOB -> 121
SDBL -> 122
SDBV -> 123

pOpAssoc :: [(POp, Word16)]
pOpAssoc = map (\op -> (op, pOpCode op)) [minBound .. maxBound]
Expand Down
34 changes: 25 additions & 9 deletions parser-typechecker/src/Unison/Runtime/Builtin.hs
Original file line number Diff line number Diff line change
Expand Up @@ -690,7 +690,6 @@ splitls = binop0 4 $ \[n0, s, n, t, l, r] ->
[ (0, ([], seqViewEmpty)),
(1, ([BX, BX], TAbss [l, r] $ seqViewElem l r))
]

splitrs = binop0 4 $ \[n0, s, n, t, l, r] ->
unbox n0 Ty.natRef n
. TLetD t UN (TPrm SPLR [n, s])
Expand Down Expand Up @@ -928,15 +927,17 @@ watch =
raise :: SuperNormal Symbol
raise =
unop0 3 $ \[r, f, n, k] ->
TMatch r . flip MatchRequest (TAbs f $ TVar f)
TMatch r
. flip MatchRequest (TAbs f $ TVar f)
. Map.singleton Ty.exceptionRef
$ mapSingleton 0
( [BX],
TAbs f
. TShift Ty.exceptionRef k
. TLetD n BX (TLit $ T "builtin.raise")
$ TPrm EROR [n, f]
)
$ mapSingleton
0
( [BX],
TAbs f
. TShift Ty.exceptionRef k
. TLetD n BX (TLit $ T "builtin.raise")
$ TPrm EROR [n, f]
)

gen'trace :: SuperNormal Symbol
gen'trace =
Expand Down Expand Up @@ -1023,6 +1024,19 @@ check'sandbox =
where
(refs, val, b) = fresh

sandbox'links :: SuperNormal Symbol
sandbox'links = Lambda [BX] . TAbs ln $ TPrm SDBL [ln]
where
ln = fresh1

value'sandbox :: SuperNormal Symbol
value'sandbox =
Lambda [BX, BX]
. TAbss [refs, val]
$ TPrm SDBV [refs, val]
where
(refs, val) = fresh

stm'atomic :: SuperNormal Symbol
stm'atomic =
Lambda [BX]
Expand Down Expand Up @@ -2168,6 +2182,8 @@ builtinLookup =
("Link.Term.toText", (Untracked, term'link'to'text)),
("STM.atomically", (Tracked, stm'atomic)),
("validateSandboxed", (Untracked, check'sandbox)),
("Value.validateSandboxed", (Tracked, value'sandbox)),
("sandboxLinks", (Tracked, sandbox'links)),
("IO.tryEval", (Tracked, try'eval))
]
++ foreignWrappers
Expand Down
11 changes: 7 additions & 4 deletions parser-typechecker/src/Unison/Runtime/MCode.hs
Original file line number Diff line number Diff line change
Expand Up @@ -61,12 +61,12 @@ import Unison.Runtime.ANF
internalBug,
packTags,
pattern TApp,
pattern TBLit,
pattern TFOp,
pattern TFrc,
pattern THnd,
pattern TLets,
pattern TLit,
pattern TBLit,
pattern TMatch,
pattern TName,
pattern TPrm,
Expand Down Expand Up @@ -390,6 +390,7 @@ data BPrim1
| TLTT -- value, Term.Link.toText
-- debug
| DBTX -- debug text
| SDBL -- sandbox link list
deriving (Show, Eq, Ord)

data BPrim2
Expand Down Expand Up @@ -424,6 +425,7 @@ data BPrim2
| TRCE -- trace
-- code
| SDBX -- sandbox
| SDBV -- sandbox Value
deriving (Show, Eq, Ord)

data MLit
Expand Down Expand Up @@ -859,7 +861,7 @@ emitSection _ _ _ _ ctx (TLit l) =
| ANF.LY {} <- l = addCount 0 1
| otherwise = addCount 1 0
emitSection _ _ _ _ ctx (TBLit l) =
addCount 0 1 . countCtx ctx . Ins (emitBLit l) . Yield $ BArg1 0
addCount 0 1 . countCtx ctx . Ins (emitBLit l) . Yield $ BArg1 0
emitSection rns grpr grpn rec ctx (TMatch v bs)
| Just (i, BX) <- ctxResolve ctx v,
MatchData r cs df <- bs =
Expand Down Expand Up @@ -1040,7 +1042,6 @@ emitLet _ _ _ _ _ _ _ (TLit l) =
fmap (Ins $ emitLit l)
emitLet _ _ _ _ _ _ _ (TBLit l) =
fmap (Ins $ emitBLit l)

-- emitLet rns grp _ _ _ ctx (TApp (FComb r) args)
-- -- We should be able to tell if we are making a saturated call
-- -- or not here. We aren't carrying the information here yet, though.
Expand Down Expand Up @@ -1190,6 +1191,8 @@ emitPOp ANF.CVLD = emitBP1 CVLD
emitPOp ANF.LOAD = emitBP1 LOAD
emitPOp ANF.VALU = emitBP1 VALU
emitPOp ANF.SDBX = emitBP2 SDBX
emitPOp ANF.SDBL = emitBP1 SDBL
emitPOp ANF.SDBV = emitBP2 SDBV
-- error call
emitPOp ANF.EROR = emitBP2 THRO
emitPOp ANF.TRCE = emitBP2 TRCE
Expand Down Expand Up @@ -1553,7 +1556,7 @@ prettySection ind sec =
. prettySection (ind + 1) pu
. foldr (\p r -> rqc p . r) id (mapToList bs)
where
rqc (i , e) =
rqc (i, e) =
showString "\n"
. shows i
. showString " ->\n"
Expand Down
86 changes: 84 additions & 2 deletions parser-typechecker/src/Unison/Runtime/Machine.hs
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,13 @@ import Unison.Builtin.Decls (exceptionRef, ioFailureRef)
import Unison.Builtin.Decls qualified as Rf
import Unison.ConstructorReference qualified as CR
import Unison.Prelude hiding (Text)
import Unison.Reference (Reference, Reference' (Builtin), toShortHash)
import Unison.Referent (pattern Con, pattern Ref)
import Unison.Reference
( Reference,
Reference' (Builtin),
isBuiltin,
toShortHash,
)
import Unison.Referent (Referent, pattern Con, pattern Ref)
import Unison.Runtime.ANF as ANF
( CompileExn (..),
Mem (..),
Expand Down Expand Up @@ -388,6 +393,14 @@ exec !env !denv !_activeThreads !ustk !bstk !k _ (BPrim1 DBTX i)
bstk <- bump bstk
bstk <$ pokeBi bstk (Util.Text.pack tx)
pure (denv, ustk, bstk, k)
exec !env !denv !_activeThreads !ustk !bstk !k _ (BPrim1 SDBL i)
| sandboxed env =
die "attempted to use sandboxed operation: sandboxLinks"
Copy link
Member

Choose a reason for hiding this comment

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

Should the error message say "sandboxLinks" here or something else?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

The error message is correct, but I'd put it in the wrong case there. It was meant for SDBL.

| otherwise = do
tl <- peekOffBi bstk i
bstk <- bump bstk
pokeS bstk . encodeSandboxListResult =<< sandboxList env tl
pure (denv, ustk, bstk, k)
exec !_ !denv !_activeThreads !ustk !bstk !k _ (BPrim1 op i) = do
(ustk, bstk) <- bprim1 ustk bstk op i
pure (denv, ustk, bstk, k)
Expand All @@ -399,6 +412,17 @@ exec !env !denv !_activeThreads !ustk !bstk !k _ (BPrim2 SDBX i j) = do
ustk <- bump ustk
poke ustk $ if b then 1 else 0
pure (denv, ustk, bstk, k)
exec !env !denv !_activeThreads !ustk !bstk !k _ (BPrim2 SDBV i j)
| sandboxed env =
die "attempted to use sandboxed operation: Value.validateSandboxed"
| otherwise = do
s <- peekOffS bstk i
v <- peekOffBi bstk j
l <- decodeSandboxArgument s
res <- checkValueSandboxing env l v
bstk <- bump bstk
poke bstk $ encodeSandboxResult res
pure (denv, ustk, bstk, k)
exec !_ !denv !_activeThreads !ustk !bstk !k _ (BPrim2 EQLU i j) = do
x <- peekOff bstk i
y <- peekOff bstk j
Expand Down Expand Up @@ -1576,6 +1600,7 @@ bprim1 !ustk !bstk TLTT _ = pure (ustk, bstk)
bprim1 !ustk !bstk LOAD _ = pure (ustk, bstk)
bprim1 !ustk !bstk VALU _ = pure (ustk, bstk)
bprim1 !ustk !bstk DBTX _ = pure (ustk, bstk)
bprim1 !ustk !bstk SDBL _ = pure (ustk, bstk)
{-# INLINE bprim1 #-}

bprim2 ::
Expand Down Expand Up @@ -1781,6 +1806,7 @@ bprim2 !ustk !bstk THRO _ _ = pure (ustk, bstk) -- impossible
bprim2 !ustk !bstk TRCE _ _ = pure (ustk, bstk) -- impossible
bprim2 !ustk !bstk CMPU _ _ = pure (ustk, bstk) -- impossible
bprim2 !ustk !bstk SDBX _ _ = pure (ustk, bstk) -- impossible
bprim2 !ustk !bstk SDBV _ _ = pure (ustk, bstk) -- impossible
{-# INLINE bprim2 #-}

yield ::
Expand Down Expand Up @@ -1949,6 +1975,22 @@ decodeSandboxArgument s = fmap join . for (toList s) $ \case
_ -> pure [] -- constructor
_ -> die "decodeSandboxArgument: unrecognized value"

encodeSandboxListResult :: [Reference] -> Sq.Seq Closure
encodeSandboxListResult =
Sq.fromList . fmap (Foreign . Wrap Rf.termLinkRef . Ref)

encodeSandboxResult :: Either [Reference] [Reference] -> Closure
encodeSandboxResult (Left rfs) =
encodeLeft . Foreign . Wrap Rf.listRef $ encodeSandboxListResult rfs
encodeSandboxResult (Right rfs) =
encodeRight . Foreign . Wrap Rf.listRef $ encodeSandboxListResult rfs

encodeLeft :: Closure -> Closure
encodeLeft = DataB1 Rf.eitherRef leftTag

encodeRight :: Closure -> Closure
encodeRight = DataB1 Rf.eitherRef rightTag

addRefs ::
TVar Word64 ->
TVar (M.Map Reference Word64) ->
Expand Down Expand Up @@ -1992,6 +2034,12 @@ codeValidate tml cc = do
extra = Foreign . Wrap Rf.textRef . Util.Text.pack $ show cs
in pure . Just $ Failure ioFailureRef msg extra

sandboxList :: CCache -> Referent -> IO [Reference]
sandboxList cc (Ref r) = do
sands <- readTVarIO $ sandbox cc
pure . maybe [] S.toList $ M.lookup r sands
sandboxList _ _ = pure []

checkSandboxing ::
CCache ->
[Reference] ->
Expand All @@ -2007,6 +2055,31 @@ checkSandboxing cc allowed0 c = do
where
allowed = S.fromList allowed0

-- Checks a Value for sandboxing. A Left result indicates that some
-- dependencies of the Value are unknown. A Right result indicates
-- builtins transitively referenced by the Value that are disallowed.
checkValueSandboxing ::
CCache ->
[Reference] ->
ANF.Value ->
IO (Either [Reference] [Reference])
checkValueSandboxing cc allowed0 v = do
sands <- readTVarIO $ sandbox cc
have <- readTVarIO $ intermed cc
let f False r
| Nothing <- M.lookup r have,
not (isBuiltin r) =
(S.singleton r, mempty)
| Just rs <- M.lookup r sands =
(mempty, rs `S.difference` allowed)
f _ _ = (mempty, mempty)
case valueLinks f v of
(miss, sbx)
| S.null miss -> pure . Right $ S.toList sbx
| otherwise -> pure . Left $ S.toList miss
where
allowed = S.fromList allowed0

cacheAdd0 ::
S.Set Reference ->
[(Reference, SuperGroup Symbol)] ->
Expand Down Expand Up @@ -2358,6 +2431,15 @@ unitTag
packTags rt 0
| otherwise = error "internal error: unitTag"

leftTag, rightTag :: Word64
(leftTag, rightTag)
| Just n <- M.lookup Rf.eitherRef builtinTypeNumbering,
et <- toEnum (fromIntegral n),
lt <- toEnum (fromIntegral Rf.eitherLeftId),
rt <- toEnum (fromIntegral Rf.eitherRightId) =
(packTags et lt, packTags et rt)
| otherwise = error "internal error: either tags"

universalCompare ::
(Foreign -> Foreign -> Ordering) ->
Closure ->
Expand Down
4 changes: 4 additions & 0 deletions parser-typechecker/src/Unison/Runtime/Serialize.hs
Original file line number Diff line number Diff line change
Expand Up @@ -449,6 +449,7 @@ instance Tag BPrim1 where
tag2word VALU = 23
tag2word TLTT = 24
tag2word DBTX = 25
tag2word SDBL = 26

word2tag 0 = pure SIZT
word2tag 1 = pure USNC
Expand Down Expand Up @@ -476,6 +477,7 @@ instance Tag BPrim1 where
word2tag 23 = pure VALU
word2tag 24 = pure TLTT
word2tag 25 = pure DBTX
word2tag 26 = pure SDBL
word2tag n = unknownTag "BPrim1" n

instance Tag BPrim2 where
Expand Down Expand Up @@ -504,6 +506,7 @@ instance Tag BPrim2 where
tag2word SDBX = 22
tag2word IXOT = 23
tag2word IXOB = 24
tag2word SDBV = 25

word2tag 0 = pure EQLU
word2tag 1 = pure CMPU
Expand All @@ -530,4 +533,5 @@ instance Tag BPrim2 where
word2tag 22 = pure SDBX
word2tag 23 = pure IXOT
word2tag 24 = pure IXOB
word2tag 25 = pure SDBV
word2tag n = unknownTag "BPrim2" n
7 changes: 6 additions & 1 deletion scheme-libs/racket/unison/boot.ss
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,10 @@
data
data-case

expand-sandbox
check-sandbox
set-sandbox

(struct-out unison-data)
(struct-out unison-termlink)
(struct-out unison-termlink-con)
Expand Down Expand Up @@ -68,6 +72,7 @@
(only-in racket/control prompt0-at control0-at)
unison/core
unison/data
unison/sandbox
unison/data-info
unison/crypto
(only-in unison/chunked-seq
Expand Down Expand Up @@ -506,7 +511,7 @@
(match rf
[(unison-data _ t (list nm))
#:when (= t unison-reference-builtin:tag)
(unison-termlink-builtin nm)]
(unison-termlink-builtin (chunked-string->string nm))]
[(unison-data _ t (list id))
#:when (= t unison-reference-derived:tag)
(match id
Expand Down
Loading
Loading