[Git][ghc/ghc][wip/nr/wasm-translation-prototypes] demonstration of unary and binary operators including comparisons
Norman Ramsey (@nrnrnr)
gitlab at gitlab.haskell.org
Thu Sep 29 16:44:47 UTC 2022
Norman Ramsey pushed to branch wip/nr/wasm-translation-prototypes at Glasgow Haskell Compiler / GHC
Commits:
893c276e by Norman Ramsey at 2022-09-29T12:44:36-04:00
demonstration of unary and binary operators including comparisons
The code is clean. The addition of a type parameter to track
the platform Boolean type is annoying, but I don't see how to
avoid it.
- - - - -
2 changed files:
- compiler/GHC/Wasm/IR.hs
- compiler/GHC/Wasm/Tx.hs
Changes:
=====================================
compiler/GHC/Wasm/IR.hs
=====================================
@@ -2,9 +2,10 @@
{-# LANGUAGE DataKinds, GADTs, RankNTypes, TypeOperators, KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TypeFamilies, ConstraintKinds #-}
module GHC.Wasm.IR
- ( WasmIR(..), (<>), pattern WasmIf, wasmReturn
+ ( WasmIR(..), (<>), pattern WasmIf32, wasmReturn
, BrTableInterval(..), inclusiveInterval
, brTableLimit
@@ -19,6 +20,8 @@ where
import GHC.Prelude
import Data.Kind
+import Data.Type.Equality
+
import GHC.Data.FastString
import GHC.Utils.Outputable hiding ((<>))
@@ -45,6 +48,14 @@ data WasmTypeTag :: WasmType -> Type where
TagI64 :: WasmTypeTag 'I64
TagF64 :: WasmTypeTag 'F64
+instance TestEquality WasmTypeTag where
+ TagI32 `testEquality` TagI32 = Just Refl
+ TagI64 `testEquality` TagI64 = Just Refl
+ TagF32 `testEquality` TagF32 = Just Refl
+ TagF64 `testEquality` TagF64 = Just Refl
+ _ `testEquality` _ = Nothing
+
+
-- | List of WebAssembly types used to describe the sequence of WebAssembly
-- values that a block of code may expect on the stack or leave on the stack.
@@ -66,58 +77,66 @@ data WasmFunctionType pre post =
-- | Representation of WebAssembly control flow.
-- Normally written as
-- @
--- WasmIR pre post
+-- WasmIR bool pre post
-- @
--- Type parameter `s` is the type of (unspecified) statements.
--- It might be instantiated with an open Cmm block or with a sequence
--- of Wasm instructions.
--- Parameter `e` is the type of expressions.
+-- Type parameter `bool` represents the Wasm type of Boolean results
-- Parameter `pre` represents the values that are expected on the
-- WebAssembly stack when the code runs, and `post` represents
-- the state of the stack on completion.
-data WasmIR :: [WasmType] -> [WasmType] -> Type where
+data WasmIR :: WasmType -> [WasmType] -> [WasmType] -> Type where
- WasmPush :: WasmTypeTag t -> WasmIR stack (t ': stack) -> WasmIR stack (t ': stack)
+ WasmPush :: WasmTypeTag t -> WasmIR bool stack (t ': stack) -> WasmIR bool stack (t ': stack)
WasmBlock :: WasmFunctionType pre post
- -> WasmIR pre post
- -> WasmIR pre post
+ -> WasmIR bool pre post
+ -> WasmIR bool pre post
WasmLoop :: WasmFunctionType pre post
- -> WasmIR pre post
- -> WasmIR pre post
+ -> WasmIR bool pre post
+ -> WasmIR bool pre post
WasmIfTop :: WasmFunctionType pre post
- -> WasmIR pre post
- -> WasmIR pre post
- -> WasmIR ('I32 ': pre) post
+ -> WasmIR bool pre post
+ -> WasmIR bool pre post
+ -> WasmIR bool (bool ': pre) post
- WasmBr :: Int -> WasmIR dropped destination -- not typechecked
- WasmFallthrough :: WasmIR dropped destination
+ WasmBr :: Int -> WasmIR bool dropped destination -- not typechecked
+ WasmFallthrough :: WasmIR bool dropped destination
-- generates no code, but has the same type as a branch
WasmBrTable :: e
-> BrTableInterval -- for testing
-> [Int] -- targets
-> Int -- default target
- -> WasmIR dropped destination
+ -> WasmIR bool dropped destination
-- invariant: the table interval is contained
-- within [0 .. pred (length targets)]
WasmReturnTop :: WasmTypeTag t
- -> WasmIR (t ': t1star) t2star -- as per type system
+ -> WasmIR bool (t ': t1star) t2star -- as per type system
- WasmActions :: s -> WasmIR stack stack -- basic block: one entry, one exit
- WasmSeq :: WasmIR pre mid -> WasmIR mid post -> WasmIR pre post
+ WasmActions :: s -> WasmIR bool stack stack -- basic block: one entry, one exit
+ WasmSeq :: WasmIR bool pre mid -> WasmIR bool mid post -> WasmIR bool pre post
----------------------------
- WasmConst :: WasmTypeTag t -> Integer -> WasmIR pre (t : pre)
+ WasmInt :: WasmTypeTag t -> Integer -> WasmIR bool pre (t : pre)
+ WasmFloat :: WasmTypeTag t -> Rational -> WasmIR bool pre (t : pre)
+
+ WasmAdd :: WasmTypeTag t -> WasmIR bool (t : t : stack) (t : stack)
+ WasmSub :: WasmTypeTag t -> WasmIR bool (t : t : stack) (t : stack)
+ WasmS_Ge :: WasmTypeTag t -> WasmIR bool (t : t : stack) (bool : stack) -- signed >=
+
+ WasmNot :: WasmTypeTag t -> WasmIR bool (t : stack) (t : stack) -- bitwise
+
+ -----
+
+ WasmCCall :: SymName -> WasmIR bool pre post -- completely untyped
+ WasmGlobalSet :: WasmTypeTag t -> SymName -> WasmIR bool (t : pre) pre
+ WasmLocalGet :: WasmTypeTag t -> Int -> WasmIR bool pre (t : pre)
+ WasmLocalSet :: WasmTypeTag t -> Int -> WasmIR bool (t : pre) pre
- WasmAdd :: WasmTypeTag t -> WasmIR (t : t : stack) (t : stack)
+ WasmLift :: (pre' ~ (t : pre), post' ~ (t : post)) =>
+ WasmTypeTag t -> WasmIR bool pre post -> WasmIR bool pre' post'
- WasmCCall :: SymName -> WasmIR pre post -- completely untyped
- WasmGlobalSet :: WasmTypeTag t -> SymName -> WasmIR (t : pre) pre
- WasmLocalGet :: WasmTypeTag t -> Int -> WasmIR pre (t : pre)
- WasmLocalSet :: WasmTypeTag t -> Int -> WasmIR (t : pre) pre
@@ -146,27 +165,27 @@ inclusiveInterval lo hi
BrTableInterval lo count
| otherwise = panic "GHC.Wasm.ControlFlow: empty interval"
-(<>) :: forall pre mid post
- . WasmIR pre mid
- -> WasmIR mid post
- -> WasmIR pre post
+(<>) :: forall bool pre mid post
+ . WasmIR bool pre mid
+ -> WasmIR bool mid post
+ -> WasmIR bool pre post
(<>) = WasmSeq
-- N.B. Fallthrough can't be optimized away because of type checking.
-- Syntactic sugar.
-pattern WasmIf :: WasmFunctionType pre post
- -> WasmIR pre ('I32 : pre)
- -> WasmIR pre post
- -> WasmIR pre post
- -> WasmIR pre post
+pattern WasmIf32 :: WasmFunctionType pre post
+ -> WasmIR 'I32 pre ('I32 : pre)
+ -> WasmIR 'I32 pre post
+ -> WasmIR 'I32 pre post
+ -> WasmIR 'I32 pre post
-pattern WasmIf ty e t f =
+pattern WasmIf32 ty e t f =
WasmPush TagI32 e `WasmSeq` WasmIfTop ty t f
-- More syntactic sugar.
-wasmReturn :: WasmTypeTag t -> WasmIR t1star (t : t1star) -> WasmIR t1star t2star
+wasmReturn :: WasmTypeTag t -> WasmIR bool t1star (t : t1star) -> WasmIR bool t1star t2star
wasmReturn tag e = WasmPush tag e `WasmSeq` WasmReturnTop tag
=====================================
compiler/GHC/Wasm/Tx.hs
=====================================
@@ -2,8 +2,12 @@
{-# LANGUAGE DataKinds, GADTs, RankNTypes, TypeOperators, KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
module GHC.Wasm.Tx
+ ( tx
+ , CG(..)
+ )
where
import GHC.Prelude
@@ -18,53 +22,96 @@ import GHC.Cmm.Expr
import GHC.Utils.Panic
import GHC.Wasm.IR
-class Monad m => CG m where
- platformWordSize :: m Int
- asType :: WasmTypeTag t -> m () -- check that type is consistent
- -- with platform word size
- asInt :: WasmTypeTag t -> m () -- insist on the platofrm integer type
+class Monad (codegen bool) => CG bool codegen where
+-- platformWordSize :: m Int
+-- asType :: WasmTypeTag t -> m () -- check that type is consistent
+-- -- with platform word size
+-- asInt :: WasmTypeTag t -> m () -- insist on the platofrm integer type
+ booleanWasmTypeTag :: codegen bool (WasmTypeTag bool)
-tx :: CG m
+tx :: CG bool codegen
=> CmmExpr
- -> (forall t . WasmTypeTag t -> WasmIR pre (t : pre) -> m r)
- -> m r
+ -> (forall t . WasmTypeTag t -> WasmIR bool '[] (t : '[]) -> codegen bool r)
+ -> codegen bool r
-- combines type checking and translation
tx expr k =
case expr of
CmmLit (CmmInt n w) -> withIntWidthTag w $ \tag -> k tag (WasmInt tag n)
CmmLit (CmmFloat x w) -> withFloatWidthTag w $ \tag -> k tag (WasmFloat tag x)
- CmmMachOp (MO_Add _w) es -> -- typecheck _w later
- binary es $ \tag code1 code2 ->
- k tag (code1 <> code2 <> WasmAdd tag)
+ CmmMachOp (MO_Add w) es -> wasmBinary w es WasmAdd k
+ CmmMachOp (MO_Sub w) es -> wasmBinary w es WasmSub k
+
+ CmmMachOp (MO_S_Ge w) es -> wasmCompare w es WasmS_Ge k
+
+ CmmMachOp (MO_Not w) es -> wasmUnary w es WasmNot k
_ -> panic "unimplemented"
+wasmBinary :: CG bool codegen
+ => CT.Width
+ -> [CmmExpr]
+ -> (forall t . WasmTypeTag t -> WasmIR bool (t : t : '[]) (t : '[]))
+ -> (forall t . WasmTypeTag t -> WasmIR bool '[] (t : '[]) -> codegen bool r)
+ -> codegen bool r
+
+wasmCompare :: forall bool codegen r . CG bool codegen
+ => CT.Width
+ -> [CmmExpr]
+ -> (forall t . WasmTypeTag t -> WasmIR bool (t : t : '[]) (bool : '[]))
+ -> ( WasmTypeTag bool -> WasmIR bool '[] (bool : '[]) -> codegen bool r)
+ -> codegen bool r
+
+wasmUnary :: CG bool codegen
+ => CT.Width
+ -> [CmmExpr]
+ -> (forall t . WasmTypeTag t -> WasmIR bool (t : '[]) (t : '[]))
+ -> (forall t . WasmTypeTag t -> WasmIR bool '[] (t : '[]) -> codegen bool r)
+ -> codegen bool r
+
+
+wasmBinary w es operator k =
+ binaryCPS es $ \tag code1 code2 ->
+ checkTagWidth tag w $ -- optional check
+ k tag (code1 <> WasmLift tag code2 <> operator tag)
+
-binary :: CG m
+wasmCompare w es operator k =
+ binaryCPS es $ \tag code1 code2 -> do
+ bool <- booleanWasmTypeTag
+ checkTagWidth bool w $
+ k bool (code1 <> WasmLift tag code2 <> operator tag)
+
+binaryCPS
+ :: forall bool codegen a . CG bool codegen
=> [CmmExpr]
-> (forall t . WasmTypeTag t
- -> WasmIR pre (t : pre)
- -> WasmIR (t : pre) (t : t : pre)
- -> m a)
- -> m a
-binary [e1, e2] k =
- tx e1 $ \tag1 m1 ->
- tx e2 $ \tag2 m2 ->
- case tag1 `testEquality` tag2 of
- Just Refl -> k tag1 (magic m1) (magic m2)
- Nothing -> panic "ill-typed Cmm"
-
-magic :: a -> b
-magic x = magic x
-
-whenEqual :: WasmTypeTag t -> WasmTypeTag t' -> (forall t . WasmTypeTag t -> a) -> a
- -- trusted code
-whenEqual TagI32 TagI32 k = k TagI32
-whenEqual TagF32 TagF32 k = k TagF32
-whenEqual TagI64 TagI64 k = k TagI64
-whenEqual TagF64 TagF64 k = k TagF64
-whenEqual _ _ _ = panic "ill-typed Cmm in Wasm translation"
+ -> WasmIR bool '[] (t : '[])
+ -> WasmIR bool '[] (t : '[])
+ -> codegen bool a)
+ -> codegen bool a
+
+binaryCPS [e1, e2] k = -- would dearly love to use do notation here
+ tx e1 $ \tag1 code1 ->
+ tx e2 $ \tag2 code2 ->
+ case tag1 `testEquality` tag2 of -- mandatory check
+ Just Refl -> k tag1 code1 code2
+ Nothing -> panic "ill-typed Cmm"
+binaryCPS _ _ = panic "wrong number of operands to binary operator in Cmm"
+
+wasmUnary w [e] operator k =
+ tx e $ \tag code -> checkTagWidth tag w $ k tag (code <> operator tag)
+wasmUnary _ _ _ _ = panic "wrong number of operands to unary operator in Cmm"
+
+----------------------------------------------------------------
+
+
+checkTagWidth :: WasmTypeTag t -> CT.Width -> a -> a
+checkTagWidth TagI32 CT.W32 a = a
+checkTagWidth TagF32 CT.W32 a = a
+checkTagWidth TagI64 CT.W64 a = a
+checkTagWidth TagF64 CT.W64 a = a
+checkTagWidth _ _ _ = panic "ill-typed Cmm (width mismatch)"
withIntWidthTag :: CT.Width -> (forall t . WasmTypeTag t -> a) -> a
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/893c276e403e2eddcc458c373d541a4f2a7c80bf
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/893c276e403e2eddcc458c373d541a4f2a7c80bf
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20220929/6a9f919d/attachment-0001.html>
More information about the ghc-commits
mailing list