[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