Fix heap pointer bounds check

src/intf/symbolic_memory_intf.ml

@@ -15,9 +15,13 @@ module type M = sig
 
   val storen : t -> address -> Smtml.Expr.t -> int -> unit
 
+  (** [validate_address m a range] verifies whether an operation starting at
+      address [a] is valid within the address range [a] to [a + range - 1]
+      (inclusive). *)
   val validate_address :
        t
     -> Smtml.Expr.t
+    -> int
     -> (Smtml.Expr.t, Trap.t) result Symbolic_choice_without_memory.t
 
   val realloc :

src/symbolic/symbolic_memory_concretizing.ml

@@ -103,21 +103,31 @@ module Backend = struct
       Hashtbl.replace m.data a' v'
     done
 
-  let validate_address m a =
+  let validate_address m a range =
     let open Symbolic_choice_without_memory in
     match Smtml.Expr.view a with
-    | Val (Num (I32 _)) -> return (Ok a) (* An i32 is a valid address *)
-    | Ptr { base; offset } -> (
+    | Val (Num (I32 _)) ->
+      (* An i32 is not a pointer to a heap chunk, so its valid *)
+      return (Ok a)
+    | Ptr { base; offset = start_offset } -> (
       let open Symbolic_value in
-      (* A pointer is valid if it's within bounds. *)
       match Hashtbl.find m.chunks base with
       | exception Not_found -> return (Error Trap.Memory_leak_use_after_free)
-      | size ->
-        let+ is_out_of_bounds = select (I32.ge_u offset size) in
+      | chunk_size ->
+        let+ is_out_of_bounds =
+          let range = const_i32 (Int32.of_int (range - 1)) in
+          (* end_offset: last byte we will read/write *)
+          let end_offset = I32.add start_offset range in
+          select
+            (Bool.or_
+               (I32.ge_u start_offset chunk_size)
+               (I32.ge_u end_offset chunk_size) )
+        in
         if is_out_of_bounds then Error Trap.Memory_heap_buffer_overflow
         else Ok a )
     | _ ->
-      (* A symbolic expression should be a valid address *)
+      (* A symbolic expression is valid, but we print to check if Ptr's are passing through here  *)
+      Log.debug2 "Saw a symbolic address: %a@." Expr.pp a;
       return (Ok a)
 
   let ptr v =

src/symbolic/symbolic_memory_make.ml

@@ -57,14 +57,14 @@ module Make (Backend : M) = struct
 
   let clone m = { data = Backend.clone m.data; size = m.size }
 
-  let must_be_valid_address m a =
+  let must_be_valid_address m a n =
     let open Symbolic_choice_without_memory in
-    let* addr = Backend.validate_address m a in
+    let* addr = Backend.validate_address m a n in
     match addr with Error t -> trap t | Ok ptr -> Backend.address ptr
 
   let load_8_s m a =
     let open Symbolic_choice_without_memory in
-    let+ a = must_be_valid_address m.data a in
+    let+ a = must_be_valid_address m.data a 1 in
     let v = Backend.loadn m.data a 1 in
     match Smtml.Expr.view v with
     | Val (Num (I8 i8)) ->
@@ -73,56 +73,65 @@ module Make (Backend : M) = struct
 
   let load_8_u m a =
     let open Symbolic_choice_without_memory in
-    let+ a = must_be_valid_address m.data a in
+    let+ a = must_be_valid_address m.data a 1 in
     let v = Backend.loadn m.data a 1 in
     match Smtml.Expr.view v with
     | Val (Num (I8 i)) -> Symbolic_value.const_i32 (Int32.of_int i)
     | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Zero_extend 24) v
 
   let load_16_s m a =
     let open Symbolic_choice_without_memory in
-    let+ a = must_be_valid_address m.data a in
+    let+ a = must_be_valid_address m.data a 2 in
     let v = Backend.loadn m.data a 2 in
     match Smtml.Expr.view v with
     | Val (Num (I32 i16)) -> Symbolic_value.const_i32 (Int32.extend_s 16 i16)
     | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Sign_extend 16) v
 
   let load_16_u m a =
     let open Symbolic_choice_without_memory in
-    let+ a = must_be_valid_address m.data a in
+    let+ a = must_be_valid_address m.data a 2 in
     let v = Backend.loadn m.data a 2 in
     match Smtml.Expr.view v with
     | Val (Num (I32 _)) -> v
     | _ -> Smtml.Expr.cvtop (Ty_bitv 32) (Zero_extend 16) v
 
+  (* TODO: Smtml should do this. Make call to Expr.simplify *)
+  let try_to_remove_extract v =
+    match Smtml.Expr.view v with
+    | Extract ({ node = Concat (({ node = Ptr _; _ } as ptr), _); _ }, 8, 4) ->
+      ptr
+    | Extract ({ node = Concat (_, ({ node = Ptr _; _ } as ptr)); _ }, 4, 0) ->
+      ptr
+    | _ -> v
+
   let load_32 m a =
     let open Symbolic_choice_without_memory in
-    let+ a = must_be_valid_address m.data a in
-    Backend.loadn m.data a 4
+    let+ a = must_be_valid_address m.data a 4 in
+    try_to_remove_extract @@ Backend.loadn m.data a 4
 
   let load_64 m a =
     let open Symbolic_choice_without_memory in
-    let+ a = must_be_valid_address m.data a in
+    let+ a = must_be_valid_address m.data a 8 in
     Backend.loadn m.data a 8
 
   let store_8 m ~addr v =
     let open Symbolic_choice_without_memory in
-    let+ a = must_be_valid_address m.data addr in
+    let+ a = must_be_valid_address m.data addr 1 in
     Backend.storen m.data a v 1
 
   let store_16 m ~addr v =
     let open Symbolic_choice_without_memory in
-    let+ a = must_be_valid_address m.data addr in
+    let+ a = must_be_valid_address m.data addr 2 in
     Backend.storen m.data a v 2
 
   let store_32 m ~addr v =
     let open Symbolic_choice_without_memory in
-    let+ a = must_be_valid_address m.data addr in
+    let+ a = must_be_valid_address m.data addr 4 in
     Backend.storen m.data a v 4
 
   let store_64 m ~addr v =
     let open Symbolic_choice_without_memory in
-    let+ a = must_be_valid_address m.data addr in
+    let+ a = must_be_valid_address m.data addr 8 in
     Backend.storen m.data a v 8
 
   let get_limit_max _m = None (* TODO *)