-
Notifications
You must be signed in to change notification settings - Fork 42
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
crucible-wasm: Adapt to new elem format in Wasm 2.0
This bumps the `haskell-wasm` commit to SPY/haskell-wasm@de40134 and does the minimum amount of work needed to make `crucible-wasm` continue to compile after these changes. For now, we do not implement full support for Wasm 2.0's new element segment features, as that would require a non-trivial amount of work to support. See #1228.
- Loading branch information
1 parent
04afc3b
commit 03d618f
Showing
2 changed files
with
24 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -404,12 +404,18 @@ installElemSegment :: | |
Wasm.ElemSegment -> | ||
InstM () | ||
installElemSegment im es@Wasm.ElemSegment{ .. } = | ||
do I32Val tblOff <- evalConst im offset | ||
do (tableIndex, offset) <- | ||
case mode of | ||
Wasm.Active idx off -> pure (idx, off) | ||
Wasm.Passive -> unimplemented "Passive element segments" | ||
Wasm.Declarative -> unimplemented "Declarative element segments" | ||
I32Val tblOff <- evalConst im offset | ||
funcIndexes <- traverse evalConstFuncIndex elements | ||
st <- lift get | ||
debug "installing element segment" | ||
debug (show es) | ||
debug (show (instTableAddrs im)) | ||
case updStore (fromIntegral tblOff) st of | ||
case updStore tableIndex funcIndexes (fromIntegral tblOff) st of | ||
Nothing -> instErr ("failed to evaluate element segment: " <> TL.pack (show es)) | ||
Just st' -> lift (put st') | ||
|
||
|
@@ -418,8 +424,8 @@ installElemSegment im [email protected]{ .. } = | |
do hdl <- Seq.lookup faddr (storeFuncs st) | ||
pure (updateFuncTable loc fty hdl ft) | ||
|
||
updStore :: Int -> Store -> Maybe Store | ||
updStore off st = | ||
updStore :: Wasm.TableIndex -> [Wasm.FuncIndex] -> Int -> Store -> Maybe Store | ||
updStore tableIndex funcIndexes off st = | ||
do (Wasm.TableType (Wasm.Limit lmin _) Wasm.FuncRef, addr) <- resolveTableIndex tableIndex im | ||
functab <- Seq.lookup addr (storeTables st) | ||
guard (toInteger off + toInteger (length funcIndexes) <= toInteger lmin) | ||
|
@@ -463,6 +469,19 @@ evalConst i [Wasm.GetGlobal idx] = | |
|
||
evalConst _ _ = instErr "expression not a constant!" | ||
|
||
-- | Evaluate a constant 'Wasm.Expression' that is expected to be a single | ||
-- 'Wasm.RefFunc' instruction, returning the underlying 'Wasm.FuncIndex'. | ||
-- Currently, this is only used when computing element segments. | ||
|
||
-- TODO: Ideally, we would merge this function with 'evalConst' above by adding | ||
-- references to functions as a first-class 'ConstantValue'. Doing so would | ||
-- require fixing https://github.com/GaloisInc/crucible/issues/1228 first, | ||
-- however. | ||
evalConstFuncIndex :: Wasm.Expression -> InstM Wasm.FuncIndex | ||
evalConstFuncIndex [Wasm.RefFunc fi] = pure fi | ||
evalConstFuncIndex e = | ||
instErr $ "expression not a function index constant: " <> fromString (show e) | ||
|
||
bindImport :: Namespace -> ModuleInstance -> Wasm.Import -> InstM ExternalValue | ||
bindImport ns i Wasm.Import{ .. } = | ||
case namespaceLookup (Wasm.Ident sourceModule) name ns of | ||
|
Submodule haskell-wasm
updated
10 files
+1 −2 | README.md | |
+61 −4 | src/Language/Wasm/Binary.hs | |
+56 −27 | src/Language/Wasm/Interpreter.hs | |
+60 −18 | src/Language/Wasm/Parser.y | |
+10 −3 | src/Language/Wasm/Structure.hs | |
+13 −17 | src/Language/Wasm/Validate.hs | |
+1 −1 | stack.yaml | |
+4 −4 | stack.yaml.lock | |
+2 −1 | tests/Test.hs | |
+9 −9 | wasm.cabal |