Skip to content

Commit

Permalink
Simplify out_of_bounds checks
Browse files Browse the repository at this point in the history
  • Loading branch information
filipeom committed Aug 1, 2024
1 parent a99b768 commit 40e5c5b
Showing 1 changed file with 3 additions and 5 deletions.
8 changes: 3 additions & 5 deletions src/symbolic/symbolic_memory_concretizing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -108,15 +108,13 @@ module Backend = struct
match Smtml.Expr.view a with
| Val (Num (I32 _)) -> return (Ok a) (* An i32 is a valid address *)
| Ptr { base; offset } -> (
let (* A pointer is valid if it's within bounds. *)
open Symbolic_value in
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 base = const_i32 base in
let ptr = I32.add base offset in
let+ is_out_of_bounds =
select (Bool.or_ (I32.lt ptr base) (I32.ge ptr (I32.add base size)))
select (Bool.or_ (I32.lt offset (const_i32 0l)) (I32.ge offset size))
in
if is_out_of_bounds then Error Trap.Memory_heap_buffer_overflow
else Ok a )
Expand Down

0 comments on commit 40e5c5b

Please sign in to comment.