[Git][ghc/ghc][wip/nr/typed-wasm-control-flow] 9 commits: first steps toward a type checker for WebAssembly
Norman Ramsey (@nrnrnr)
gitlab at gitlab.haskell.org
Mon Aug 8 21:30:59 UTC 2022
Norman Ramsey pushed to branch wip/nr/typed-wasm-control-flow at Glasgow Haskell Compiler / GHC
Commits:
94f2ed0b by Norman Ramsey at 2022-08-05T19:11:14-04:00
first steps toward a type checker for WebAssembly
- - - - -
4643e751 by Norman Ramsey at 2022-08-08T15:13:44-04:00
add type signatures; apply hlint
- - - - -
1db49958 by Norman Ramsey at 2022-08-08T15:14:04-04:00
snapshot prototype validator
- - - - -
cbc6fe77 by Norman Ramsey at 2022-08-08T15:14:39-04:00
remove deprecated quote mark
- - - - -
e9e1d0dd by Norman Ramsey at 2022-08-08T15:14:52-04:00
clean up main test file
- - - - -
48569247 by Norman Ramsey at 2022-08-08T15:17:28-04:00
about-face on validation
- - - - -
7ce4fa23 by Norman Ramsey at 2022-08-08T15:17:28-04:00
add README to test suite
- - - - -
5467c9c9 by Norman Ramsey at 2022-08-08T17:30:30-04:00
deal with new compiler warnings
- - - - -
4e5da206 by Norman Ramsey at 2022-08-08T17:30:41-04:00
add draft emitter for typed wasm
- - - - -
6 changed files:
- + compiler/GHC/Wasm/Builder.hs
- compiler/GHC/Wasm/ControlFlow.hs
- compiler/GHC/Wasm/ControlFlow/FromCmm.hs
- compiler/ghc.cabal.in
- + testsuite/tests/wasm/should_run/control-flow/README.md
- testsuite/tests/wasm/should_run/control-flow/WasmControlFlow.hs
Changes:
=====================================
compiler/GHC/Wasm/Builder.hs
=====================================
@@ -0,0 +1,75 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module GHC.Wasm.Builder
+ ( toIndented
+ , MyExpr(..), MyActions(..)
+ )
+where
+
+-- early rough draft of emitter from WebAssembly to clang .s code
+
+import GHC.Prelude
+
+import Data.ByteString.Builder (Builder)
+import Data.List (intersperse)
+import Data.Monoid
+
+import qualified Data.ByteString.Builder as BS
+
+import GHC.Utils.Panic
+
+import GHC.Wasm.ControlFlow hiding ((<>))
+
+defaultIndent :: Builder
+defaultIndent = " "
+
+toIndented :: WasmControl MyActions MyExpr pre post -> Builder
+toIndented s = printWithIndent mempty s <> "\n"
+
+wasmFunctionType :: WasmFunctionType pre post -> Builder
+wasmFunctionType (WasmFunctionType TypeListNil TypeListNil) = ""
+wasmFunctionType (WasmFunctionType TypeListNil (TypeListCons t TypeListNil)) = tagBuilder t
+wasmFunctionType _ = panic "function type needs to be externalized"
+
+tagBuilder :: WasmTypeTag a -> Builder
+tagBuilder TagI32 = "i32"
+tagBuilder TagF32 = "f32"
+
+
+printWithIndent :: Builder -> WasmControl MyActions MyExpr pre post -> Builder
+printWithIndent indent s = print s
+ where print, outdent :: WasmControl MyActions MyExpr pre post -> Builder
+ newline :: Builder -> Builder -> Builder
+ (<+>) :: Builder -> Builder -> Builder
+ ty = wasmFunctionType
+
+ print (WasmFallthrough `WasmSeq` s) = print s
+ print (s `WasmSeq` WasmFallthrough) = print s
+ print (WasmIfTop t s WasmFallthrough) =
+ "br_if" <+> ty t `newline` outdent s `newline` "end_if"
+ print (WasmIfTop t WasmFallthrough s) =
+ "br_if" <+> ty t `newline` "else" `newline` outdent s `newline` "end_if"
+
+ print (WasmPush _ _) = "i32.const 42"
+ print (WasmBlock t s) = "block" <+> ty t `newline` outdent s `newline` "end_block"
+ print (WasmLoop t s) = "loop" <+> ty t `newline` outdent s `newline` "end_loop"
+ print (WasmIfTop t ts fs) = "if" <+> ty t `newline` outdent ts `newline`
+ "else" `newline` outdent fs `newline` "end_if"
+ print (WasmBr l) = "br" <+> BS.intDec l
+ print (WasmBrTable e _ ts t) =
+ myExpr e `newline` "br_table {" <+>
+ mconcat (intersperse ", " [BS.intDec i | i <- ts <> [t]]) <+>
+ "}"
+ print (WasmReturnTop _) = "return"
+ print (WasmActions as) = myActions as
+ print (s `WasmSeq` s') = print s `newline` print s'
+
+ newline s s' = s <> "\n" <> indent <> s'
+ outdent s = defaultIndent <> printWithIndent (indent <> defaultIndent) s
+ s <+> s' = s <> " " <> s'
+
+
+newtype MyExpr = MyExpr { myExpr :: Builder }
+
+newtype MyActions = MyActions { myActions :: Builder }
=====================================
compiler/GHC/Wasm/ControlFlow.hs
=====================================
@@ -56,7 +56,7 @@ Description : Representation of control-flow portion of the WebAssembly instruct
data TypeList :: [WasmType] -> Type where
TypeListNil :: TypeList '[]
- TypeListCons :: WasmTypeTag t -> TypeList ts -> TypeList (t ': ts)
+ TypeListCons :: WasmTypeTag t -> TypeList ts -> TypeList (t : ts)
data WasmFunctionType pre post =
WasmFunctionType { ft_pops :: TypeList pre
@@ -66,10 +66,11 @@ data WasmFunctionType pre post =
type Push t = WasmFunctionType '[] '[t]
data WasmType = I32 | F32 -- more could be added
+ deriving (Eq, Show)
data WasmTypeTag :: WasmType -> Type where
- TagI32 :: WasmTypeTag I32
- TagF32 :: WasmTypeTag F32
+ TagI32 :: WasmTypeTag 'I32
+ TagF32 :: WasmTypeTag 'F32
data WasmControl :: Type -> Type -> [WasmType] -> [WasmType] -> Type where
@@ -84,7 +85,7 @@ data WasmControl :: Type -> Type -> [WasmType] -> [WasmType] -> Type where
WasmIfTop :: WasmFunctionType pre post
-> WasmControl s e pre post
-> WasmControl s e pre post
- -> WasmControl s e (I32 ': pre) post
+ -> WasmControl s e ('I32 ': pre) post
WasmBr :: Int -> WasmControl s e dropped destination -- not typechecked
WasmFallthrough :: WasmControl s e dropped destination
=====================================
compiler/GHC/Wasm/ControlFlow/FromCmm.hs
=====================================
@@ -21,7 +21,6 @@ import GHC.Prelude hiding (succ)
import Data.Function
import Data.List (sortBy)
---import Data.Semigroup
import qualified Data.Tree as Tree
import GHC.Cmm
@@ -161,6 +160,9 @@ structuredControl :: forall expr stmt .
structuredControl platform txExpr txBlock g =
doTree returns dominatorTree emptyContext
where
+ gwd :: GraphWithDominators CmmNode
+ gwd = graphWithDominators g
+
dominatorTree :: Tree.Tree CfgNode-- Dominator tree in which children are sorted
-- with highest reverse-postorder number first
dominatorTree = fmap blockLabeled $ sortTree $ gwdDominatorTree gwd
@@ -180,9 +182,9 @@ structuredControl platform txExpr txBlock g =
where selectedChildren = case lastNode x of
CmmSwitch {} -> children
-- N.B. Unlike `if`, translation of Switch uses only labels.
- _ -> filter hasMergeRoot $ children
+ _ -> filter hasMergeRoot children
loopContext = LoopHeadedBy (entryLabel x) `inside`
- (context `withFallthrough` (entryLabel x))
+ (context `withFallthrough` entryLabel x)
hasMergeRoot = isMergeNode . Tree.rootLabel
nodeWithin fty x (y_n:ys) (Just zlabel) context =
@@ -227,11 +229,13 @@ structuredControl platform txExpr txBlock g =
| otherwise = doTree fty (subtreeAt to) context -- inline the code here
where i = index to (enclosing context)
+ generatesIf :: CmmBlock -> Bool
generatesIf x = case flowLeaving platform x of Conditional {} -> True
_ -> False
---- everything else is utility functions
+ treeEntryLabel :: Tree.Tree CfgNode -> Label
treeEntryLabel = entryLabel . Tree.rootLabel
sortTree :: Tree.Tree Label -> Tree.Tree Label
@@ -252,6 +256,7 @@ structuredControl platform txExpr txBlock g =
dominates :: Label -> Label -> Bool
-- Domination relation (not just immediate domination)
+ blockmap :: LabelMap CfgNode
GMany NothingO blockmap NothingO = g_graph g
blockLabeled l = findLabelIn l blockmap
@@ -268,12 +273,13 @@ structuredControl platform txExpr txBlock g =
isMergeLabel l = setMember l mergeBlockLabels
isMergeNode = isMergeLabel . entryLabel
+ isBackward :: Label -> Label -> Bool
isBackward from to = rpnum to <= rpnum from -- self-edge counts as a backward edge
subtreeAt label = findLabelIn label subtrees
subtrees :: LabelMap (Tree.Tree CfgNode)
subtrees = addSubtree mapEmpty dominatorTree
- where addSubtree map (t@(Tree.Node root children)) =
+ where addSubtree map t@(Tree.Node root children) =
foldl addSubtree (mapInsert (entryLabel root) t map) children
mergeBlockLabels :: LabelSet
@@ -297,19 +303,19 @@ structuredControl platform txExpr txBlock g =
| otherwise = addToList (from :) to pm
isLoopHeader = isHeaderLabel . entryLabel
- isHeaderLabel = \l -> setMember l headers -- loop headers
+ isHeaderLabel = (`setMember` headers) -- loop headers
where headers :: LabelSet
headers = foldMap headersPointedTo blockmap
headersPointedTo block =
setFromList [label | label <- successors block,
dominates label (entryLabel block)]
+ index :: Label -> [ContainingSyntax] -> Int
index _ [] = panic "destination label not in evaluation context"
index label (frame : context)
| label `matchesFrame` frame = 0
| otherwise = 1 + index label context
- gwd = graphWithDominators g
rpnum = gwdRPNumber gwd
dominates lbl blockname =
lbl == blockname || dominatorsMember lbl (gwdDominatorsOf gwd blockname)
=====================================
compiler/ghc.cabal.in
=====================================
@@ -805,6 +805,7 @@ Library
GHC.Utils.Ppr.Colour
GHC.Utils.TmpFs
GHC.Utils.Trace
+ GHC.Wasm.Builder
GHC.Wasm.ControlFlow
GHC.Wasm.ControlFlow.FromCmm
=====================================
testsuite/tests/wasm/should_run/control-flow/README.md
=====================================
@@ -0,0 +1,12 @@
+Tests the basic infrastructure used to translate Cmm control flow to WebAssembly control flow:
+
+ - Check a Cmm control-flow graph to see if it is reducible.
+
+ - Convert an irreducible control-flow graph to an equivalent reducible control-flow graph.
+
+ - Interpret both Cmm control-flow graphs and WebAssembly programs using a stream of bits to determine the direction of each conditional and `switch`. Confirm that source and target programs take the same actions and make the same decisions.
+
+The tests dump a lot of information about the code under test, including the number of execution paths tested. Samples in `WasmControlFlow.stdout`.
+
+The source codes for the tested control-flow graphs are written in a mix of Haskell and Cmm; they are found in directory `src`.
+
=====================================
testsuite/tests/wasm/should_run/control-flow/WasmControlFlow.hs
=====================================
@@ -1,9 +1,3 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TupleSections #-}
-
-
module Main where
import Control.Monad
@@ -38,14 +32,6 @@ import LoadCmmGroup
import RunCmm
import RunWasm
-data TestMode = ReducibilityTest | SplittingTest | TranslationTest
-
-testMode :: String -> TestMode
-testMode s = case s of "-r" -> ReducibilityTest
- "-s" -> SplittingTest
- "-t" -> TranslationTest
- _ -> error "mode should be -r or -t"
-
main :: IO ()
main = do
libdir : modeString : files <- getArgs
@@ -61,40 +47,6 @@ main = do
liftIO $ do
codes <- mapM (allTests $ targetPlatform dflags) (zip files groups)
exitWith $ foldl combineExits exitZero codes
-{-
- labeled_groups = [(path, group)
- | (path, groups) <- zip files groups, group <- groups]
- run :: (CmmGraph -> IO a) -> IO [(FilePath, a)]
- run f = concat <$>
- mapM (fmap unroll . concatMapGraphs platform (const f)) labeled_groups
- runGrouped :: (CmmGraph -> IO a) -> IO [(FilePath, [a])]
- runGrouped f =
- mergeLike <$> mapM (concatMapGraphs platform (const f)) labeled_groups
- unroll :: (FilePath, [a]) -> [(FilePath, a)]
- unroll (path, as) = [(path, a) | a <- as]
- mergeLike :: [(FilePath, [a])] -> [(FilePath, [a])]
- mergeLike pairs =
- [(path, matching path) | path <- nub (map fst pairs)]
- where matching path = [a | (path', as) <- pairs, path == path', a <- as]
- liftIO $ case testMode modeString of
- ReducibilityTest -> do
- analyses <- runGrouped (return . reducibility . graphWithDominators)
- let dump (path, results) = do
- putStr $ path ++ ": "
- case (number (== Reducible), number (== Irreducible)) of
- (0, 0) -> putStrLn $ "no code"
- (0, n) -> putStrLn $ show n ++ " irreducible"
- (n, 0) -> putStrLn $ show n ++ " reducible"
- (r, i) -> putStrLn $ show r ++ " reducible, " ++ show i ++ " irreducible"
- where number p = length $ filter p $ results
- mapM_ dump analyses
- SplittingTest -> do
- reductions <- run testNodeSplitting
- mutilations <- run (return . testGraphMutilation)
- results <- liftM2 (++) (mapM (analyze isIdentical) reductions)
- (mapM (analyze isDifferent) mutilations)
- exitWith $ foldl combineExits exitZero results
--}
allTests :: Platform -> (FilePath, [CmmGroup]) -> IO ExitCode
allTests platform (path, groups) =
@@ -104,7 +56,15 @@ allTests platform (path, groups) =
tests :: [Platform -> (FilePath, [CmmGroup]) -> IO ExitCode]
tests = [reducibilityTest, splittingTest, translationTest]
-reducibilityTest, splittingTest, translationTest :: Platform -> (FilePath, [CmmGroup]) -> IO ExitCode
+reducibilityTest, splittingTest, translationTest
+ :: Platform -> (FilePath, [CmmGroup]) -> IO ExitCode
+
+
+
+
+----------------------------------------------------------------
+
+-- | Counts the number of reducible and irreducible CFGs in each group
reducibilityTest platform (path, groups) = do
analyses <- runGrouped (return . reducibility . graphWithDominators) platform groups
@@ -121,54 +81,20 @@ reducibilityTest platform (path, groups) = do
dump analyses
return exitZero
+----------------------------------------------------------------
+
+-- Convert each input graph to a reducible graph via node splitting,
+-- run control-flow--path tests to confirm they behave the same.
+-- Run similar tests that compare each graph with a mutilated version,
+-- to confirm that the tests do in fact detect when graphs are different.
+
splittingTest platform (path, groups) = do
reductions <- catMaybes <$> runGrouped testNodeSplitting platform groups
mutilations <- runGrouped (return . testGraphMutilation path) platform groups
codes <- liftM2 (++) (mapM (analyze "node splitting" path isIdentical) reductions)
- (mapM (analyze "mutilation" path isDifferent) mutilations)
+ (mapM (analyze "mutilation" path isDifferent) mutilations)
return $ foldl combineExits exitZero codes
-translationTest platform (path, groups) = do
- txs <- runGrouped (testTranslation platform) platform groups
- codes <- mapM (analyze "WebAssembly translation" path isIdentical) txs
- return $ foldl combineExits exitZero codes
-
-
-
-
-runGrouped :: (CmmGraph -> IO a) -> Platform -> [CmmGroup] -> IO [a]
-runGrouped f platform groups = concat <$> mapM (concatMapGraphs platform (const f)) groups
-
-concatMapGraphs :: Monad m
- => Platform
- -> (Platform -> CmmGraph -> m a)
- -> CmmGroup
- -> m [a]
-concatMapGraphs platform f group =
- catMaybes <$> mapM (decl . cmmCfgOptsProc False) group
- where decl (CmmData {}) = return Nothing
- decl (CmmProc _h _entry _registers graph) =
- do a <- f platform graph
- return $ Just a
-
-count :: [a] -> String -> String
-count xs thing = case length xs of
- 1 -> "1 " ++ thing
- n -> show n ++ " " ++ thing ++ "s"
-
-
-data Outcome = Identical { npaths :: Int }
- | Different { different :: [(Trace, Trace)], nsame :: Int }
-type Trace = [Event Stmt Expr]
-
-isDifferent, isIdentical :: Outcome -> Bool
-
-isDifferent (Different {}) = True
-isDifferent _ = False
-
-isIdentical (Identical {}) = True
-isIdentical _ = False
-
testNodeSplitting :: CmmGraph -> IO (Maybe Outcome)
testNodeSplitting original_graph = do
reducible_graph <- fmap gwd_graph $ runUniqSM $
@@ -184,38 +110,57 @@ testGraphMutilation :: FilePath -> CmmGraph -> Outcome
testGraphMutilation path graph =
compareWithEntropy (runcfg graph) (runcfg $ mutilate path graph) $ cfgEntropy graph
+-- | Changes the graph's entry point to one of the entry point's successors.
+-- Panics if the input graph has only one block.
+mutilate :: FilePath -> CmmGraph -> CmmGraph
+mutilate path g =
+ case filter (/= entry_label) $ successors entry_block of
+ (lbl:_) -> CmmGraph lbl (g_graph g)
+ [] -> error $ "cannot mutilate control-flow graph in file " ++ path
+ where entry_label = g_entry g
+ entry_block = mapFindWithDefault (error "no entry block") entry_label $ graphMap g
+
+----------------------------------------------------------------
+
+-- Translate each input graph to WebAssembly, then run
+-- control-flow--path tests to confirm the translation behaves the
+-- same as the original.
+
+translationTest platform (path, groups) = do
+ txs <- runGrouped (testTranslation platform) platform groups
+ codes <- mapM (analyze "WebAssembly translation" path isIdentical) txs
+ return $ foldl combineExits exitZero codes
+
testTranslation :: Platform -> CmmGraph -> IO Outcome
testTranslation platform big_switch_graph = do
real_graph <- runUniqSM $ cmmImplementSwitchPlans platform big_switch_graph
reducible_graph <- fmap gwd_graph $ runUniqSM $
asReducible $ graphWithDominators real_graph
- let wasm = structuredControlIncludingNonTail platform expr stmt reducible_graph
+ let wasm = structuredControl platform expr stmt reducible_graph
return $ compareWithEntropy (runcfg real_graph) (runwasm wasm) $
cfgEntropy reducible_graph
- where structuredControlIncludingNonTail = structuredControl -- XXX
-runcfg :: CmmGraph -> BitConsumer Stmt Expr ()
-runcfg = evalGraph stmt expr
+----------------------------------------------------------------
-runwasm :: WasmControl Stmt Expr pre post -> BitConsumer Stmt Expr ()
-runwasm = evalWasm
+-- Outcomes of comparisons
-runUniqSM :: UniqSM a -> IO a
-runUniqSM m = do
- us <- mkSplitUniqSupply 'g'
- return (initUs_ us m)
+data Outcome = Identical { npaths :: Int }
+ | Different { different :: [(Trace, Trace)], nsame :: Int }
+type Trace = [Event Stmt Expr]
-type Entropy = [[Bool]]
+isDifferent, isIdentical :: Outcome -> Bool
+
+isDifferent (Different {}) = True
+isDifferent _ = False
+
+isIdentical (Identical {}) = True
+isIdentical _ = False
----------------------------------------------------------------
-mutilate :: FilePath -> CmmGraph -> CmmGraph
-mutilate path g =
- case filter (/= entry_label) $ successors entry_block of
- (lbl:_) -> CmmGraph lbl (g_graph g)
- [] -> error $ "cannot mutilate control-flow graph in file " ++ path
- where entry_label = g_entry g
- entry_block = mapFindWithDefault (error "no entry block") entry_label $ graphMap g
+-- Comparisons of execution paths
+
+type Entropy = [[Bool]]
compareWithEntropy :: BitConsumer Stmt Expr ()
-> BitConsumer Stmt Expr ()
@@ -247,19 +192,6 @@ compareRuns a b bits =
cfgEntropy :: CmmGraph -> Entropy
cfgEntropy = map traceBits . cmmPaths
-unimp :: String -> a
-unimp s = error $ s ++ " not implemented"
-
-----------------------------------------------------------------
-
-combineExits :: ExitCode -> ExitCode -> ExitCode
-exitZero :: ExitCode
-
-exitZero = ExitSuccess
-combineExits ExitSuccess e = e
-combineExits e _ = e
-
-
analyze :: String -> FilePath -> (Outcome -> Bool) -> Outcome -> IO ExitCode
analyze what path isGood outcome = do
putStrLn $ display $ path ++ ", " ++ what ++ ": " ++ case outcome of
@@ -275,3 +207,49 @@ analyze what path isGood outcome = do
return $ ExitFailure 1
where display s = if isGood outcome then s ++ ", as expected"
else "(FAULT!) " ++ s
+
+----------------------------------------------------------------
+
+-- Other test-running infrastructure
+
+runGrouped :: (CmmGraph -> IO a) -> Platform -> [CmmGroup] -> IO [a]
+runGrouped f platform groups = concat <$> mapM (concatMapGraphs platform (const f)) groups
+
+concatMapGraphs :: Monad m
+ => Platform
+ -> (Platform -> CmmGraph -> m a)
+ -> CmmGroup
+ -> m [a]
+concatMapGraphs platform f group =
+ catMaybes <$> mapM (decl . cmmCfgOptsProc False) group
+ where decl (CmmData {}) = return Nothing
+ decl (CmmProc _h _entry _registers graph) =
+ do a <- f platform graph
+ return $ Just a
+
+count :: [a] -> String -> String
+count xs thing = case length xs of
+ 1 -> "1 " ++ thing
+ n -> show n ++ " " ++ thing ++ "s"
+
+runcfg :: CmmGraph -> BitConsumer Stmt Expr ()
+runcfg = evalGraph stmt expr
+
+runwasm :: WasmControl Stmt Expr pre post -> BitConsumer Stmt Expr ()
+runwasm = evalWasm
+
+runUniqSM :: UniqSM a -> IO a
+runUniqSM m = do
+ us <- mkSplitUniqSupply 'g'
+ return (initUs_ us m)
+
+----------------------------------------------------------------
+
+-- ExitCode as monoid
+
+combineExits :: ExitCode -> ExitCode -> ExitCode
+exitZero :: ExitCode
+
+exitZero = ExitSuccess
+combineExits ExitSuccess e = e
+combineExits e _ = e
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/961ad4583a6aa038da16948b1016279a3706d91c...4e5da2060be0daed39f4d8f6e4060e87a9474fe5
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/961ad4583a6aa038da16948b1016279a3706d91c...4e5da2060be0daed39f4d8f6e4060e87a9474fe5
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/20220808/8837309d/attachment-0001.html>
More information about the ghc-commits
mailing list