Merge pull request #1232 from GaloisInc/T1227-latest-haskell-wasm-commit

`crucible-wasm`: Build and test with the latest `haskell-wasm` commit

crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs

@@ -273,6 +273,9 @@ valueTypeToType Wasm.I32 = Some (BVRepr (knownNat @32))
 valueTypeToType Wasm.I64 = Some (BVRepr (knownNat @64))
 valueTypeToType Wasm.F32 = Some (FloatRepr SingleFloatRepr)
 valueTypeToType Wasm.F64 = Some (FloatRepr DoubleFloatRepr)
+-- See https://github.com/GaloisInc/crucible/issues/1228
+valueTypeToType Wasm.Func   = error "Func reference types are not currently supported"
+valueTypeToType Wasm.Extern = error "Extern reference types are not currently supported"
 
 valueTypesToContext :: [Wasm.ValueType] -> Some (Assignment TypeRepr)
 valueTypesToContext = fromList . map valueTypeToType
@@ -385,7 +388,11 @@ computeDataSegment ::
   Wasm.DataSegment ->
   InstM (GlobalVar WasmMem, Word32, LBS.ByteString)
 computeDataSegment i Wasm.DataSegment{ .. } =
-  do st <- lift get
+  do (memIndex, offset) <-
+       case dataMode of
+         Wasm.ActiveData memIndex offset -> pure (memIndex, offset)
+         Wasm.PassiveData -> unimplemented "Passive data segments"
+     st <- lift get
      case resolveMemIndex memIndex i of
        Nothing -> instErr ("Could not resolve memory index " <> fromString (show memIndex))
        Just (_,_,addr) ->
@@ -401,12 +408,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')
 
@@ -415,8 +428,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)
@@ -460,6 +473,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

crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs

@@ -32,7 +32,6 @@ import qualified Lang.Crucible.LLVM.MemModel.Generic as G
 import qualified Lang.Crucible.LLVM.MemModel.Partial as Partial
 
 import What4.Interface
-import What4.InterpretedFloatingPoint
 
 import Lang.Crucible.Wasm.Utils
 

crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs

@@ -334,6 +334,11 @@ translateFunction fty [email protected]{ .. } im st hdl =
   setupLocal Wasm.F64 =
     do r <- newReg (App (DoubleLit 0.0))
        modify (addLocal r)
+  -- See https://github.com/GaloisInc/crucible/issues/1228
+  setupLocal Wasm.Func =
+    unimplemented "Func reference values"
+  setupLocal Wasm.Extern =
+    unimplemented "Extern reference values"
 
   genReturn :: WasmGenerator s ret (Expr WasmExt s ret)
   genReturn = computeReturn (handleReturnType hdl) (Wasm.results fty)
@@ -547,13 +552,12 @@ genInstruction genReturn im st ctrlStack instr =
             Nothing -> panic "genInstruction: Call" ["Could not resolve function address " ++ show addr]
             Just (SomeHandle h) -> invokeFn fty (handleType h) (App (HandleLit h))
 
-    Wasm.CallIndirect tidx ->
-      case resolveTypeIndex tidx im of
-        Nothing -> panic "genInstruction: CallIndirect" ["Could not resolve type index " ++ show tidx]
+    Wasm.CallIndirect tableIdx typeIdx ->
+      case resolveTypeIndex typeIdx im of
+        Nothing -> panic "genInstruction: CallIndirect" ["Could not resolve type index " ++ show typeIdx]
         Just fty ->
-          -- NB, table index hard-coded to 0 in Wasm 1.0
-          case resolveTableIndex 0 im of
-            Nothing -> panic "genInstruction: CallIndirect" ["Could not resolve table index 0"]
+          case resolveTableIndex tableIdx im of
+            Nothing -> panic "genInstruction: CallIndirect" ["Could not resolve table index " ++ show tableIdx]
             Just (_tty, tbladdr) ->
               case Seq.lookup tbladdr (storeTables st) of
                 Nothing -> panic "genInstruction: CallIndirect" ["Could not resolve table address " ++ show tbladdr]
@@ -569,7 +573,12 @@ genInstruction genReturn im st ctrlStack instr =
     Wasm.Drop ->
       void $ popStack
 
-    Wasm.Select ->
+    -- The `select` instruction includes an optional value type, which indicates
+    -- the type of its first and second operands. We do not currently make use
+    -- of this type, however, as crucible-wasm's implementation is simple enough
+    -- where the types of all possible stack values can be inferred without any
+    -- additional type information.
+    Wasm.Select _mbValTypes ->
       do c <- popTest
          y <- popStack
          x <- popStack
@@ -613,11 +622,11 @@ genInstruction genReturn im st ctrlStack instr =
             Just (ConstantGlobal _) -> panic "genInstruction: SetGlobal" ["setGlobal of constant global"]
             Just (MutableGlobal gv) -> writeGlobal gv =<< checkStackVal (globalType gv) =<< popStack
 
-    Wasm.CurrentMemory ->
+    Wasm.MemorySize ->
       do gv <- getMemVar im st
          pushStack =<< extensionStmt (Wasm_MemSize gv)
 
-    Wasm.GrowMemory ->
+    Wasm.MemoryGrow ->
       do gv <- getMemVar im st
          n <- popInteger32
          void $ extensionStmt (Wasm_MemGrow gv n)
@@ -801,6 +810,25 @@ genInstruction genReturn im st ctrlStack instr =
     -- IReinterpretF BitSize
     -- FReinterpretI BitSize
 
+    -- RefNull ElemType
+    -- RefIsNull
+    -- RefFunc FuncIndex
+
+    -- TableInit TableIndex ElemIndex
+    -- TableGrow TableIndex
+    -- TableSize TableIndex
+    -- TableFill TableIndex
+    -- TableGet TableIndex
+    -- TableSet TableIndex
+    -- TableCopy TableIndex TableIndex
+
+    -- MemoryFill
+    -- MemoryCopy
+    -- MemoryInit DataIndex
+
+    -- ElemDrop ElemIndex
+    -- DataDrop DataIndex
+
     _ -> unimplemented $ unwords ["Instruction not implemented", show instr]
 
 invokeFn ::

crucible-wasm/test-data/elem.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.

crucible-wasm/test-data/elem.wast

@@ -0,0 +1,141 @@
+;; Test the element section
+;;
+;; Adapted from the elem test case in
+;;
+;;   https://github.com/WebAssembly/spec/blob/351d8b1026a2a820e88baae54557c43e775fd5a5/test/core/elem.wast
+
+;; Syntax
+(module
+  (table $t 10 funcref)
+  (func $f)
+  (func $g)
+
+  ;; Active
+  (elem (table $t) (i32.const 0) funcref)
+  (elem (table $t) (i32.const 0) funcref (ref.func $f) (ref.func $g))
+  (elem (table $t) (i32.const 0) func)
+  (elem (table $t) (i32.const 0) func $f $g)
+  (elem (table $t) (offset (i32.const 0)) funcref)
+  (elem (table $t) (offset (i32.const 0)) func $f $g)
+  (elem (table 0) (i32.const 0) func)
+  (elem (table 0x0) (i32.const 0) func $f $f)
+  (elem (table 0x000) (offset (i32.const 0)) func)
+  (elem (table 0) (offset (i32.const 0)) func $f $f)
+  (elem (table $t) (i32.const 0) func)
+  (elem (table $t) (i32.const 0) func $f $f)
+  (elem (table $t) (offset (i32.const 0)) func)
+  (elem (table $t) (offset (i32.const 0)) func $f $f)
+  (elem (offset (i32.const 0)))
+  (elem (offset (i32.const 0)) funcref (ref.func $f) (ref.func $g))
+  (elem (offset (i32.const 0)) func $f $f)
+  (elem (offset (i32.const 0)) $f $f)
+  (elem (i32.const 0))
+  (elem (i32.const 0) funcref (ref.func $f) (ref.func $g))
+  (elem (i32.const 0) func $f $f)
+  (elem (i32.const 0) $f $f)
+  (elem (i32.const 0) funcref (item (ref.func $f)) (item (ref.func $g)))
+
+  (elem $a1 (table $t) (i32.const 0) funcref)
+  (elem $a2 (table $t) (i32.const 0) funcref (ref.func $f) (ref.func $g))
+  (elem $a3 (table $t) (i32.const 0) func)
+  (elem $a4 (table $t) (i32.const 0) func $f $g)
+  (elem $a9 (table $t) (offset (i32.const 0)) funcref)
+  (elem $a10 (table $t) (offset (i32.const 0)) func $f $g)
+  (elem $a11 (table 0) (i32.const 0) func)
+  (elem $a12 (table 0x0) (i32.const 0) func $f $f)
+  (elem $a13 (table 0x000) (offset (i32.const 0)) func)
+  (elem $a14 (table 0) (offset (i32.const 0)) func $f $f)
+  (elem $a15 (table $t) (i32.const 0) func)
+  (elem $a16 (table $t) (i32.const 0) func $f $f)
+  (elem $a17 (table $t) (offset (i32.const 0)) func)
+  (elem $a18 (table $t) (offset (i32.const 0)) func $f $f)
+  (elem $a19 (offset (i32.const 0)))
+  (elem $a20 (offset (i32.const 0)) funcref (ref.func $f) (ref.func $g))
+  (elem $a21 (offset (i32.const 0)) func $f $f)
+  (elem $a22 (offset (i32.const 0)) $f $f)
+  (elem $a23 (i32.const 0))
+  (elem $a24 (i32.const 0) funcref (ref.func $f) (ref.func $g))
+  (elem $a25 (i32.const 0) func $f $f)
+  (elem $a26 (i32.const 0) $f $f)
+)
+
+(module
+  (func $f)
+  (func $g)
+
+  (table $t funcref (elem (ref.func $f) (ref.func $g) (ref.func $g)))
+)
+
+
+;; Basic use
+
+(module
+  (table 10 funcref)
+  (func $f)
+  (elem (i32.const 0) $f)
+)
+
+(module
+  (table 10 funcref)
+  (func $f)
+  (elem (i32.const 0) $f)
+  (elem (i32.const 3) $f)
+  (elem (i32.const 7) $f)
+  (elem (i32.const 5) $f)
+  (elem (i32.const 3) $f)
+)
+
+(module
+  (type $out-i32 (func (result i32)))
+  (table 10 funcref)
+  (elem (i32.const 7) $const-i32-a)
+  (elem (i32.const 9) $const-i32-b)
+  (func $const-i32-a (type $out-i32) (i32.const 65))
+  (func $const-i32-b (type $out-i32) (i32.const 66))
+  (func (export "call-7") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 7))
+  )
+  (func (export "call-9") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 9))
+  )
+)
+(assert_return (invoke "call-7") (i32.const 65))
+(assert_return (invoke "call-9") (i32.const 66))
+
+;; Corner cases
+
+(module
+  (table 10 funcref)
+  (func $f)
+  (elem (i32.const 9) $f)
+)
+
+(module
+  (table 0 funcref)
+  (elem (i32.const 0))
+)
+
+(module
+  (table 0 0 funcref)
+  (elem (i32.const 0))
+)
+
+(module
+  (table 20 funcref)
+  (elem (i32.const 20))
+)
+
+;; Two elements target the same slot
+
+(module
+  (type $out-i32 (func (result i32)))
+  (table 10 funcref)
+  (elem (i32.const 9) $const-i32-a)
+  (elem (i32.const 9) $const-i32-b)
+  (func $const-i32-a (type $out-i32) (i32.const 65))
+  (func $const-i32-b (type $out-i32) (i32.const 66))
+  (func (export "call-overwritten") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 9))
+  )
+)
+(assert_return (invoke "call-overwritten") (i32.const 66))

crucible-wasm/test-data/select.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.