Add write permission bit to array elements.

The `astore` instruction now checks the write permission bit.

Add writability parameter to `doAllocateArray`.

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

@@ -424,7 +424,7 @@ instance Concretize JVMRefType where
 instance Concretize JVMArrayType where
   type Concrete JVMArrayType = Vector (Maybe CValue)
   concretize (C.RV x) = do
-    let (C.RV vec) = x Ctx.! Ctx.i2of3
+    let (C.RV vec) = x Ctx.! Ctx.i2of4
     vm <- V.mapM (concretize @JVMValueType . C.RV) vec
     return (Just vm)
 

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

@@ -873,7 +873,8 @@ doStaticFieldWritable sym jc globals fid val =
 ppFieldId :: J.FieldId -> String
 ppFieldId fid = J.unClassName (J.fieldIdClass fid) ++ "." ++ J.fieldIdName fid
 
--- | Write a value at an index of an array reference.
+-- | Write a value at an index of an array reference. The write
+-- permission bit is not checked.
 doArrayStore ::
   IsSymInterface sym =>
   sym ->
@@ -888,9 +889,9 @@ doArrayStore sym globals ref idx val =
      obj <- EvalStmt.readRef sym jvmIntrinsicTypes objectRepr ref' globals
      let msg2 = C.GenericSimError "Object is not an array"
      arr <- C.readPartExpr sym (C.unVB (C.unroll obj Ctx.! Ctx.i2of2)) msg2
-     let vec = C.unRV (arr Ctx.! Ctx.i2of3)
+     let vec = C.unRV (arr Ctx.! Ctx.i2of4)
      let vec' = vec V.// [(idx, val)]
-     let arr' = Control.Lens.set (Ctx.ixF Ctx.i2of3) (C.RV vec') arr
+     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
 
@@ -947,7 +948,7 @@ doArrayLoad sym globals ref idx =
      -- TODO: define a 'projectVariant' function in the OverrideSim monad
      let msg2 = C.GenericSimError "Array load: object is not an array"
      arr <- C.readPartExpr sym (C.unVB (C.unroll obj Ctx.! Ctx.i2of2)) msg2
-     let vec = C.unRV (arr Ctx.! Ctx.i2of3)
+     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
@@ -985,13 +986,15 @@ doAllocateArray ::
   sym ->
   C.HandleAllocator ->
   JVMContext -> Int {- ^ array length -} -> J.Type {- ^ element type -} ->
+  (Int -> Bool) {- ^ per-index writability -} ->
   C.SymGlobalState sym ->
   IO (C.RegValue sym JVMRefType, C.SymGlobalState sym)
-doAllocateArray sym halloc jc len elemTy globals =
+doAllocateArray sym halloc jc len elemTy mut globals =
   do len' <- liftIO $ W4.bvLit sym w32 (BV.mkBV w32 (toInteger len))
      let vec = V.replicate len unassignedJVMValue
      rep <- makeJVMTypeRep sym globals jc elemTy
-     let arr = Ctx.Empty Ctx.:> C.RV len' Ctx.:> C.RV vec Ctx.:> C.RV rep
+     let ws = V.generate len (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)
      ref <- C.freshRefCell halloc objectRepr

crucible-jvm/src/Lang/Crucible/JVM/Translation/Class.hs

@@ -666,7 +666,7 @@ getObjectType obj =
       -- must be an array object
       let marr = App $ ProjectVariant knownRepr Ctx.i2of2 unr
       arr <- assertedJustExpr marr "must be instance or array"
-      return $ App $ GetStruct arr Ctx.i3of3 knownRepr
+      return $ App $ GetStruct arr Ctx.i4of4 knownRepr
   }
 
 
@@ -1010,7 +1010,9 @@ mkJVMArrayObject ::
   JVMGenerator s ret (JVMObject s)
 mkJVMArrayObject count vec aty =
   do ty <- makeJVMTypeRep aty
-     let ctx = Ctx.empty `Ctx.extend` count `Ctx.extend` vec `Ctx.extend` ty
+     let w = App (BoolLit True) -- new arrays default to writable
+     let ws = App (VectorReplicate knownRepr (App (BvToNat w32 count)) w)
+     let ctx = Ctx.empty `Ctx.extend` count `Ctx.extend` vec `Ctx.extend` ws `Ctx.extend` ty
      let arr = App (MkStruct knownRepr ctx)
      let uobj = injectVariant Ctx.i2of2 arr
      pure $ App $ RollRecursive knownRepr knownRepr uobj
@@ -1021,11 +1023,11 @@ arrayIdx :: JVMObject s
   -> JVMInt s
   -- ^ index into the array
   -> JVMGenerator s ret (Expr JVM s JVMValueType)
-arrayIdx obj idx = do
-     let uobj = App (UnrollRecursive knownRepr knownRepr obj)
+arrayIdx obj idx =
+  do let uobj = App (UnrollRecursive knownRepr knownRepr obj)
      let marr = App (ProjectVariant knownRepr Ctx.i2of2 uobj)
      arr <- assertedJustExpr marr "array index: not a valid array"
-     let vec = App (GetStruct arr Ctx.i2of3 knownRepr)
+     let vec = App (GetStruct arr Ctx.i2of4 knownRepr)
      -- TODO: assert 0 <= idx < length arr
      let val = App (VectorGetEntry knownRepr vec (App (BvToNat w32 idx)))
      return val
@@ -1039,10 +1041,13 @@ arrayUpdate obj idx val = do
   let uobj = App (UnrollRecursive knownRepr knownRepr obj)
   let marr = App (ProjectVariant knownRepr Ctx.i2of2 uobj)
   arr <- assertedJustExpr marr "array update: not a valid array"
-  let vec = App (GetStruct arr Ctx.i2of3 knownRepr)
+  let ws = App (GetStruct arr Ctx.i3of4 knownRepr)
+  let writable = App (VectorGetEntry knownRepr ws (App (BvToNat w32 idx)))
+  assertExpr writable "astore: array not writable"
+  let vec = App (GetStruct arr Ctx.i2of4 knownRepr)
      -- TODO: assert 0 <= idx < length arr
   let vec' = App (VectorSetEntry knownRepr vec (App (BvToNat w32 idx)) val)
-  let arr' = App (SetStruct knownRepr arr Ctx.i2of3 vec')
+  let arr' = App (SetStruct knownRepr arr Ctx.i2of4 vec')
   let uobj' = App (InjectVariant knownRepr Ctx.i2of2 arr')
   let obj' = App (RollRecursive knownRepr knownRepr uobj')
   return obj'
@@ -1053,7 +1058,7 @@ arrayLength obj = do
   let uobj = App (UnrollRecursive knownRepr knownRepr obj)
   let marr = App (ProjectVariant knownRepr Ctx.i2of2 uobj)
   arr <- assertedJustExpr marr "array length: not a valid array"
-  let len = App (GetStruct arr Ctx.i1of3 knownRepr)
+  let len = App (GetStruct arr Ctx.i1of4 knownRepr)
   return len
 
 

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

@@ -175,10 +175,16 @@ type JVMInstanceType =
     ::> JVMClassType
   )
 
--- | An array value is a length, a vector of values,
--- and an element type.
+-- | An array value is a length, a vector of values, a vector of write
+-- permission bits, and an element type.
 type JVMArrayType =
-  StructType (EmptyCtx ::> JVMIntType ::> VectorType JVMValueType ::> JVMTypeRepType)
+  StructType (
+    EmptyCtx
+    ::> JVMIntType
+    ::> VectorType JVMValueType
+    ::> VectorType BoolType
+    ::> JVMTypeRepType
+  )
 
 -- | An object is either a class instance or an array.
 type JVMObjectImpl =