Skip to content

Commit

Permalink
Merge pull request #4355 from unisonweb/topic/scheme-sandbox
Browse files Browse the repository at this point in the history
Fill out more scheme builtins
  • Loading branch information
dolio authored Oct 25, 2023
2 parents d5e809b + 0dbc19d commit d425300
Show file tree
Hide file tree
Showing 36 changed files with 1,455 additions and 812 deletions.
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"
| 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

0 comments on commit d425300

Please sign in to comment.