From 40e5c5bcaf1b8aea5a6a757b2d63e997350a38b3 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 1 Aug 2024 18:41:43 +0200 Subject: [PATCH] Simplify out_of_bounds checks --- src/symbolic/symbolic_memory_concretizing.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/symbolic/symbolic_memory_concretizing.ml b/src/symbolic/symbolic_memory_concretizing.ml index 19156eb66..6006298bb 100644 --- a/src/symbolic/symbolic_memory_concretizing.ml +++ b/src/symbolic/symbolic_memory_concretizing.ml @@ -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 )