[Git][ghc/ghc][wip/nr/wasm-translation-prototypes] 4 commits: early Tx prototype with CmmLit
Norman Ramsey (@nrnrnr)
gitlab at gitlab.haskell.org
Thu Sep 29 16:34:40 UTC 2022
Norman Ramsey pushed to branch wip/nr/wasm-translation-prototypes at Glasgow Haskell Compiler / GHC
Commits:
067d1541 by Norman Ramsey at 2022-09-29T10:13:57-04:00
early Tx prototype with CmmLit
- - - - -
aae3a173 by Norman Ramsey at 2022-09-29T11:34:28-04:00
Tx builds with magic
- - - - -
0d1fb92c by Norman Ramsey at 2022-09-29T12:32:52-04:00
a thing that compiles
- - - - -
6deab9c1 by Norman Ramsey at 2022-09-29T12:34:25-04:00
clean binary and comparison
- - - - -
3 changed files:
- compiler/GHC/Wasm/IR.hs
- + compiler/GHC/Wasm/Tx.hs
- compiler/ghc.cabal.in
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 ((<>))
@@ -31,9 +34,9 @@ Description : Representation of control-flow portion of the WebAssembly instruct
-- | WebAssembly type of a WebAssembly value that WebAssembly code
-- could either expect on the evaluation stack or leave on the evaluation
--- stack. At present we support only 32-bit values.
+-- stack.
-data WasmType = I32 | F32
+data WasmType = I32 | F32 | I64 | F64
deriving (Eq, Show)
@@ -42,6 +45,16 @@ data WasmType = I32 | F32
data WasmTypeTag :: WasmType -> Type where
TagI32 :: WasmTypeTag 'I32
TagF32 :: WasmTypeTag 'F32
+ 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.
@@ -64,54 +77,63 @@ 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 bool stack stack -- basic block: one entry, one exit
+ WasmSeq :: WasmIR bool pre mid -> WasmIR bool mid post -> WasmIR bool pre post
+
+ ----------------------------
+
+ 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 >=
+
+ 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
- WasmActions :: s -> WasmIR stack stack -- basic block: one entry, one exit
- WasmSeq :: WasmIR pre mid -> WasmIR mid post -> WasmIR pre post
+ WasmLift :: (pre' ~ (t : pre), post' ~ (t : post)) =>
+ WasmTypeTag t -> WasmIR bool pre post -> WasmIR bool pre' post'
- WasmAdd :: WasmTypeTag t -> WasmIR (t : t : stack) (t : stack)
- 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
data BrTableInterval
@@ -139,27 +161,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
=====================================
@@ -0,0 +1,118 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DataKinds, GADTs, RankNTypes, TypeOperators, KindSignatures #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module GHC.Wasm.Tx
+ ( tx
+ , CG(..)
+ )
+where
+
+import GHC.Prelude
+
+import Data.Type.Equality
+--import Data.Kind
+
+import qualified GHC.Cmm.Type as CT
+import GHC.Cmm.Expr
+--import GHC.Data.FastString
+--import GHC.Utils.Outputable hiding ((<>))
+import GHC.Utils.Panic
+import GHC.Wasm.IR
+
+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 bool codegen
+ => CmmExpr
+
+ -> (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 -> 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
+
+ _ -> 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
+
+
+wasmBinary w es operator k =
+ binaryCPS es $ \tag code1 code2 ->
+ checkTagWidth tag w $ -- optional check
+ k tag (code1 <> WasmLift tag code2 <> operator tag)
+
+
+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 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 machine operator in Cmm"
+
+
+--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"
+
+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
+withIntWidthTag CT.W32 k = k TagI32
+withIntWidthTag CT.W64 k = k TagI64
+withIntWidthTag w _ = panic $ "width " ++ show w ++ " not supported on wasm target"
+
+withFloatWidthTag :: CT.Width -> (forall t . WasmTypeTag t -> a) -> a
+withFloatWidthTag CT.W32 k = k TagF32
+withFloatWidthTag CT.W64 k = k TagF64
+withFloatWidthTag w _ = panic $ "width " ++ show w ++ " not supported on wasm target"
=====================================
compiler/ghc.cabal.in
=====================================
@@ -809,6 +809,7 @@ Library
GHC.Wasm.ControlFlow.FromCmm
GHC.Wasm.ControlFlow.ToAsm
GHC.Wasm.IR
+ GHC.Wasm.Tx
Language.Haskell.Syntax
Language.Haskell.Syntax.Basic
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4b48a635fd36b5ae4f07cc1ba332b9b56d954dd1...6deab9c16233434be431d717a7026ffaec1929dd
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4b48a635fd36b5ae4f07cc1ba332b9b56d954dd1...6deab9c16233434be431d717a7026ffaec1929dd
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/2d0417c4/attachment-0001.html>
More information about the ghc-commits
mailing list