Vec arrays

crucible-jvm/src/Lang/Crucible/JVM/Overrides.hs

@@ -87,6 +87,7 @@ import qualified Lang.Crucible.Simulator.GlobalState   as C
 import qualified Lang.Crucible.Simulator.OverrideSim   as C
 import qualified Lang.Crucible.Simulator.RegValue      as C
 import qualified Lang.Crucible.Simulator.RegMap        as C
+import qualified Lang.Crucible.Simulator.VecValue      as C
 
 import qualified Lang.Crucible.Analysis.Postdom        as C
 import qualified Lang.Crucible.Utils.MuxTree           as C
@@ -431,7 +432,7 @@ instance Concretize JVMArrayType where
   type Concrete JVMArrayType = Vector (Maybe CValue)
   concretize (C.RV x) = do
     let (C.RV vec) = x Ctx.! Ctx.i2of4
-    vm <- V.mapM (concretize @JVMValueType . C.RV) vec
+    vm <- V.mapM (concretize @JVMValueType) =<< liftIO (C.vecValToVec vec)
     return (Just vm)
 
 

crucible-jvm/src/Lang/Crucible/JVM/Simulate.hs

@@ -7,6 +7,7 @@ Maintainer       : sweirich@galois.com
 Stability        : provisional
 -}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
@@ -73,6 +74,7 @@ import qualified Lang.Crucible.Simulator.GlobalState as C
 import qualified Lang.Crucible.Simulator.RegMap as C (eqReference)
 import qualified Lang.Crucible.Simulator.CallFrame as C
 import qualified Lang.Crucible.Simulator.EvalStmt as EvalStmt (readRef, alterRef)
+import qualified Lang.Crucible.Simulator.VecValue as C
 
 
 -- what4
@@ -95,6 +97,10 @@ import           Lang.Crucible.JVM.Overrides
 import qualified Lang.JVM.Codebase as JCB
 
 
+-- | Constraints on the symbolic backends
+type IsJVMSymBackend sym bak = (IsSymBackend sym bak, C.VecSize sym (W4.SymExpr sym (BaseBVType 32)))
+
+
 {-
    This module is in two parts, the first part includes functions for translating
    JVM code to Crucible CFGs.  The second part sets up the Crucible simulation
@@ -897,7 +903,7 @@ doArrayStore bak globals ref idx val =
      let msg2 = C.GenericSimError "Object is not an array"
      arr <- C.readPartExpr bak (C.unVB (C.unroll obj Ctx.! Ctx.i2of2)) msg2
      let vec = C.unRV (arr Ctx.! Ctx.i2of4)
-     let vec' = vec V.// [(idx, val)]
+     vec' <- C.vecValSetEntryConcrete bak vec idx (C.RV val)
      let arr' = Control.Lens.set (Ctx.ixF Ctx.i2of4) (C.RV vec') arr
      let obj' = C.RolledType (C.injectVariant sym knownRepr Ctx.i2of2 arr')
      EvalStmt.alterRef sym jvmIntrinsicTypes objectRepr ref' (W4.justPartExpr sym obj') globals
@@ -956,10 +962,8 @@ doArrayLoad bak globals ref idx =
      let msg2 = C.GenericSimError "Array load: object is not an array"
      arr <- C.readPartExpr bak (C.unVB (C.unroll obj Ctx.! Ctx.i2of2)) msg2
      let vec = C.unRV (arr Ctx.! Ctx.i2of4)
-     let msg3 = C.GenericSimError $ "Array load: index out of bounds: " ++ show idx
-     case vec V.!? idx of
-       Just val -> return val
-       Nothing -> C.addFailedAssertion bak msg3
+     C.RV res <- C.vecValGetEntryConcrete bak vec idx
+     pure res
 
 -- | Allocate an instance of the given class in the global state. All
 -- of the fields are initialized to 'unassignedJVMValue'.
@@ -990,7 +994,7 @@ doAllocateObject bak halloc jc cname mut globals =
 -- | Allocate an array in the global state. All of the elements are
 -- initialized to 'unassignedJVMValue'.
 doAllocateArray ::
-  (IsSymBackend sym bak) =>
+  (IsJVMSymBackend sym bak) =>
   bak ->
   C.HandleAllocator ->
   JVMContext -> Int {- ^ array length -} -> J.Type {- ^ element type -} ->
@@ -1000,9 +1004,9 @@ doAllocateArray ::
 doAllocateArray bak halloc jc len elemTy mut globals =
   do let sym = backendGetSym bak
      len' <- liftIO $ W4.bvLit sym w32 (BV.mkBV w32 (toInteger len))
-     let vec = V.replicate len unassignedJVMValue
+     vec <- C.vecValReplicate sym len' (C.RV unassignedJVMValue) -- XXX: it would be better to use vecValUninit here, but the types are slightly different
      rep <- makeJVMTypeRep sym globals jc elemTy
-     let ws = V.generate len (W4.backendPred sym . mut)
+     let ws = C.vecValLit (V.generate len (C.RV . W4.backendPred sym . mut))
      let arr = Ctx.Empty Ctx.:> C.RV len' Ctx.:> C.RV vec Ctx.:> C.RV ws Ctx.:> C.RV rep
      let repr = Ctx.Empty Ctx.:> instanceRepr Ctx.:> arrayRepr
      let obj = C.RolledType (C.injectVariant sym repr Ctx.i2of2 arr)

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Cast.hs

@@ -41,6 +41,7 @@ import           Lang.Crucible.Backend
 import           Lang.Crucible.Simulator (SimErrorReason(AssertFailureSimError))
 import           Lang.Crucible.Simulator.OverrideSim
 import           Lang.Crucible.Simulator.RegMap
+import           Lang.Crucible.Simulator.VecValue
 import           Lang.Crucible.Types
 
 import           Lang.Crucible.LLVM.MemModel.Partial (ptrToBv)
@@ -120,7 +121,9 @@ castLLVMRet fnm bak (LLVMPointerRepr w) (BVRepr w')
     Right (ValCast (liftIO . ptrToBv bak err))
 castLLVMRet fnm bak (VectorRepr tp) (VectorRepr tp')
   = do ValCast f <- castLLVMRet fnm bak tp tp'
-       Right (ValCast (traverse f))
+       let
+          cvt g xs = vecValLit <$> (traverse (fmap RV . g . unRV) =<< liftIO (vecValToVec xs))
+       Right (ValCast (cvt f))
 castLLVMRet fnm bak (StructRepr ctx) (StructRepr ctx')
   = do ArgCast tf <- castLLVMArgs fnm bak ctx' ctx
        Right (ValCast (\vals ->

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs

@@ -50,6 +50,7 @@ import           Lang.Crucible.Types
 import           Lang.Crucible.Simulator.OverrideSim
 import           Lang.Crucible.Simulator.RegMap
 import           Lang.Crucible.Simulator.SimError (SimErrorReason(AssertFailureSimError))
+import           Lang.Crucible.Simulator.VecValue
 
 import           Lang.Crucible.LLVM.Bytes (Bytes(..), bitsToBytes)
 import           Lang.Crucible.LLVM.DataLayout (noAlignment)
@@ -1496,7 +1497,7 @@ llvmVectorMap ::
     IsSymInterface sym =>
     RegEntry sym (VectorType (BVType intSz)) ->
     RegEntry sym (VectorType (BVType intSz)) ->
-    OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))) ->
+    OverrideSim p sym ext r args ret (RegValue sym (VectorType (BVType intSz)))) ->
   -- | The size of the vector type.
   NatRepr vecSz ->
   -- | The size of the integer type.
@@ -1562,33 +1563,39 @@ callX86_pclmulqdq _mvar
   (regValue -> ys)
   (regValue -> imm) =
     ovrWithBackend $ \bak -> do
-      unless (V.length xs == 2) $
+      let len_xs = vecValSizeConcrete xs
+      let len_ys = vecValSizeConcrete ys
+      unless (len_xs == 2) $
          liftIO $ addFailedAssertion bak $ AssertFailureSimError
           ("Vector length mismatch in llvm.x86.pclmulqdq intrinsic")
-          (unwords ["Expected <2 x i64>, but got vector of length", show (V.length xs)])
-      unless (V.length ys == 2) $
+          (unwords ["Expected <2 x i64>, but got vector of length", show len_xs])
+      unless (len_ys == 2) $
          liftIO $ addFailedAssertion bak $ AssertFailureSimError
           ("Vector length mismatch in llvm.x86.pclmulqdq intrinsic")
-          (unwords ["Expected <2 x i64>, but got vector of length", show (V.length ys)])
+          (unwords ["Expected <2 x i64>, but got vector of length", show len_ys])
       case BV.asUnsigned <$> asBV imm of
         Just byte ->
           do let xidx = if byte .&. 0x01 == 0 then 0 else 1
              let yidx = if byte .&. 0x10 == 0 then 0 else 1
              let sym = backendGetSym bak
-             liftIO $ doPcmul sym (xs V.! xidx) (ys V.! yidx)
+             liftIO $
+              do
+                x <- vecValGetEntryConcrete bak xs xidx
+                y <- vecValGetEntryConcrete bak ys yidx
+                doPcmul sym x y
         _ ->
             liftIO $ addFailedAssertion bak $ AssertFailureSimError
                ("Illegal selector argument to llvm.x86.pclmulqdq")
                (unwords ["Expected concrete value but got", show (printSymExpr imm)])
   where
 
-  doPcmul :: sym -> SymBV sym 64 -> SymBV sym 64 -> IO (V.Vector (SymBV sym 64))
-  doPcmul sym x y =
+  doPcmul :: sym -> RegValue' sym (BVType 64) -> RegValue' sym (BVType 64) -> IO (VecVal (RegValue' sym) (BVType 64))
+  doPcmul sym (RV x) (RV y) =
     do r <- carrylessMultiply sym x y
        lo <- bvTrunc sym (knownNat @64) r
        hi <- bvSelect sym (knownNat @64) (knownNat @64) r
        -- NB, little endian because X86
-       return $ V.fromList [ lo, hi ]
+       return $ vecValLit $ V.fromList [ RV lo, RV hi ]
 
 callStoreudq
   :: ( IsSymInterface sym
@@ -1604,10 +1611,11 @@ callStoreudq mvar
   (regValue -> vec) =
     ovrWithBackend $ \bak -> do
       mem <- readGlobal mvar
-      unless (V.length vec == 16) $
+      let len = vecValSizeConcrete vec
+      unless (len == 16) $
          liftIO $ addFailedAssertion bak $ AssertFailureSimError
           ("Vector length mismatch in stored_qu intrinsic.")
-          (unwords ["Expected <16 x i8>, but got vector of length", show (V.length vec)])
+          (unwords ["Expected <16 x i8>, but got vector of length", show len])
       mem' <- liftIO $ doStore
                 bak
                 mem
@@ -2116,6 +2124,8 @@ callLoadRelative mvar w (regValue -> ptr) (regValue -> offsetInWords32) = do
 
 -- | The semantics of an LLVM vector reduce intrinsic.
 callVectorReduce ::
+  forall sym tp p ext r args ret.
+  IsExprBuilder sym =>
   -- | The operation which performs the reduction (e.g., addition,
   -- multiplication, etc.)
   (RegValue sym tp -> RegValue sym tp -> IO (RegValue sym tp)) ->
@@ -2126,7 +2136,11 @@ callVectorReduce ::
   RegEntry sym (VectorType tp) ->
   OverrideSim p sym ext r args ret (RegValue sym tp)
 callVectorReduce reduceOp identityVal (regValue -> vec) =
-  liftIO $ V.foldM reduceOp identityVal vec
+  getSymInterface >>= \sym ->
+  liftIO $ unRV <$> vecValFold sym reduceOp' (RV identityVal) vec
+  where
+  reduceOp' :: RegValue' sym tp -> RegValue' sym tp -> IO (RegValue' sym tp)
+  reduceOp' (RV x) (RV y) = RV <$> reduceOp x y
 
 callVectorReduceAdd ::
   (IsSymInterface sym, 1 <= intSz) =>
@@ -2221,22 +2235,26 @@ callVectorReduceUmin intSz vec = do
 
 -- | The semantics of an LLVM vector map intrinsic.
 callVectorMap ::
+  IsExprBuilder sym =>
   -- | The operation to apply when mapping (e.g., @umin@, @smin@, etc.)
   (RegValue sym tp -> RegValue sym tp -> IO (RegValue sym tp)) ->
   -- | The first vector to map over.
   RegEntry sym (VectorType tp) ->
   -- | The second vector to map over.
   RegEntry sym (VectorType tp) ->
   -- | The result of mapping over the vectors.
-  OverrideSim p sym ext r args ret (V.Vector (RegValue sym tp))
+  OverrideSim p sym ext r args ret (RegValue sym (VectorType tp))
 callVectorMap mapOp (regValue -> vec1) (regValue -> vec2) =
-  liftIO $ V.zipWithM mapOp vec1 vec2
+  getSymInterface >>= \sym ->
+  liftIO $ vecValZipWith sym mapOp' vec1 vec2
+  where
+  mapOp' (RV x) (RV y) = RV <$> mapOp x y
 
 callVectorMapSmax ::
   (IsSymInterface sym, 1 <= intSz) =>
   RegEntry sym (VectorType (BVType intSz)) ->
   RegEntry sym (VectorType (BVType intSz)) ->
-  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))
+  OverrideSim p sym ext r args ret (RegValue sym (VectorType (BVType intSz)))
 callVectorMapSmax vec1 vec2 = do
   sym <- getSymInterface
   callVectorMap (bvSmax sym) vec1 vec2
@@ -2245,7 +2263,7 @@ callVectorMapSmin ::
   (IsSymInterface sym, 1 <= intSz) =>
   RegEntry sym (VectorType (BVType intSz)) ->
   RegEntry sym (VectorType (BVType intSz)) ->
-  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))
+  OverrideSim p sym ext r args ret (RegValue sym (VectorType (BVType intSz)))
 callVectorMapSmin vec1 vec2 = do
   sym <- getSymInterface
   callVectorMap (bvSmin sym) vec1 vec2
@@ -2254,7 +2272,7 @@ callVectorMapUmax ::
   (IsSymInterface sym, 1 <= intSz) =>
   RegEntry sym (VectorType (BVType intSz)) ->
   RegEntry sym (VectorType (BVType intSz)) ->
-  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))
+  OverrideSim p sym ext r args ret (RegValue sym (VectorType (BVType intSz)))
 callVectorMapUmax vec1 vec2 = do
   sym <- getSymInterface
   callVectorMap (bvUmax sym) vec1 vec2
@@ -2263,7 +2281,7 @@ callVectorMapUmin ::
   (IsSymInterface sym, 1 <= intSz) =>
   RegEntry sym (VectorType (BVType intSz)) ->
   RegEntry sym (VectorType (BVType intSz)) ->
-  OverrideSim p sym ext r args ret (V.Vector (SymBV sym intSz))
+  OverrideSim p sym ext r args ret (RegValue sym (VectorType (BVType intSz)))
 callVectorMapUmin vec1 vec2 = do
   sym <- getSymInterface
   callVectorMap (bvUmin sym) vec1 vec2

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs

@@ -53,6 +53,7 @@ import           Lang.Crucible.Simulator.ExecutionTree
 import           Lang.Crucible.Simulator.OverrideSim
 import           Lang.Crucible.Simulator.RegMap
 import           Lang.Crucible.Simulator.SimError
+import           Lang.Crucible.Simulator.VecValue
 
 import           Lang.Crucible.LLVM.Bytes
 import           Lang.Crucible.LLVM.DataLayout
@@ -672,7 +673,9 @@ callPrintf mvar
       case parseDirectives formatStr of
         Left err -> overrideError $ AssertFailureSimError "Format string parsing failed" err
         Right ds -> do
-          ((str, n), mem') <- liftIO $ runStateT (executeDirectives (printfOps bak valist) ds) mem
+          ((str, n), mem') <- liftIO $
+            do valist' <- vecValToVec valist
+               runStateT (executeDirectives (printfOps bak valist') ds) mem
           writeGlobal mvar mem'
           h <- printHandle <$> getContext
           liftIO $ BS.hPutStr h str
@@ -681,7 +684,7 @@ callPrintf mvar
 printfOps :: ( IsSymBackend sym bak, HasLLVMAnn sym, HasPtrWidth wptr
              , ?memOpts :: MemOptions )
           => bak
-          -> V.Vector (AnyValue sym)
+          -> V.Vector (RegValue' sym AnyType)
           -> PrintfOperations (StateT (MemImpl sym) IO)
 printfOps bak valist =
   let sym = backendGetSym bak in
@@ -691,7 +694,7 @@ printfOps bak valist =
 
   , printfGetInteger = \i sgn _len ->
      case valist V.!? (i-1) of
-       Just (AnyValue (LLVMPointerRepr w) p@(LLVMPointer _blk bv)) ->
+       Just (RV (AnyValue (LLVMPointerRepr w) p@(LLVMPointer _blk bv))) ->
          do isBv <- liftIO (Ptr.ptrIsBv sym p)
             liftIO $ assert bak isBv $
               AssertFailureSimError
@@ -701,7 +704,7 @@ printfOps bak valist =
               return $ BV.asSigned w <$> asBV bv
             else
               return $ BV.asUnsigned <$> asBV bv
-       Just (AnyValue tpr _) ->
+       Just (RV (AnyValue tpr _)) ->
          lift $ addFailedAssertion bak
               $ AssertFailureSimError
                 "Type mismatch in printf"
@@ -714,10 +717,10 @@ printfOps bak valist =
 
   , printfGetFloat = \i _len ->
      case valist V.!? (i-1) of
-       Just (AnyValue (FloatRepr (_fi :: FloatInfoRepr fi)) x) ->
+       Just (RV (AnyValue (FloatRepr (_fi :: FloatInfoRepr fi)) x)) ->
          do xr <- liftIO (iFloatToReal @_ @fi sym x)
             return (asRational xr)
-       Just (AnyValue tpr _) ->
+       Just (RV (AnyValue tpr _)) ->
          lift $ addFailedAssertion bak
               $ AssertFailureSimError
                 "Type mismatch in printf."
@@ -730,10 +733,10 @@ printfOps bak valist =
 
   , printfGetString  = \i numchars ->
      case valist V.!? (i-1) of
-       Just (AnyValue PtrRepr ptr) ->
+       Just (RV (AnyValue PtrRepr ptr)) ->
            do mem <- get
               liftIO $ CStr.loadString bak mem ptr numchars
-       Just (AnyValue tpr _) ->
+       Just (RV (AnyValue tpr _)) ->
          lift $ addFailedAssertion bak
               $ AssertFailureSimError
                 "Type mismatch in printf."
@@ -746,9 +749,9 @@ printfOps bak valist =
 
   , printfGetPointer = \i ->
      case valist V.!? (i-1) of
-       Just (AnyValue PtrRepr ptr) ->
+       Just (RV (AnyValue PtrRepr ptr)) ->
          return $ show (G.ppPtr ptr)
-       Just (AnyValue tpr _) ->
+       Just (RV (AnyValue tpr _)) ->
          lift $ addFailedAssertion bak
               $ AssertFailureSimError
                 "Type mismatch in printf."
@@ -761,7 +764,7 @@ printfOps bak valist =
 
   , printfSetInteger = \i len v ->
      case valist V.!? (i-1) of
-       Just (AnyValue PtrRepr ptr) ->
+       Just (RV (AnyValue PtrRepr ptr)) ->
          do mem <- get
             case len of
               Len_Byte  -> do
@@ -793,7 +796,7 @@ printfOps bak valist =
                      $ Unsupported GHC.callStack
                      $ unwords ["Unsupported size modifier in %n conversion:", show len]
 
-       Just (AnyValue tpr _) ->
+       Just (RV (AnyValue tpr _)) ->
          lift $ addFailedAssertion bak
               $ AssertFailureSimError
                 "Type mismatch in printf."