diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml index c93f5b690..455250f1d 100644 --- a/src/concolic/concolic_wasm_ffi.ml +++ b/src/concolic/concolic_wasm_ffi.ml @@ -98,7 +98,7 @@ module M : let ptr (v : Value.int32) : int32 Choice.t = match view v.symbolic with - | Ptr (b, _) -> Choice.return b + | Ptr { base; _ } -> Choice.return base | _ -> Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v.symbolic; Choice.bind (abort ()) (fun () -> assert false) @@ -111,7 +111,7 @@ module M : Choice.bind (i32 base) (fun (base : int32) -> Choice.return { Concolic_value.concrete = base - ; symbolic = Expr.make (Ptr (base, Symbolic_value.const_i32 0l)) + ; symbolic = Expr.ptr base (Symbolic_value.const_i32 0l) } ) (* WHAT ???? *) (* Choice.with_thread (fun t : Value.int32 -> *) diff --git a/src/symbolic/symbolic.ml b/src/symbolic/symbolic.ml index ec778b683..841edc337 100644 --- a/src/symbolic/symbolic.ml +++ b/src/symbolic/symbolic.ml @@ -63,10 +63,10 @@ struct match Expr.view a with (* Avoid unecessary re-hashconsing and allocation when the value is already concrete. *) - | Val _ | Ptr (_, { node = Val _; _ }) -> return a - | Ptr (base, offset) -> + | Val _ | Ptr { offset = { node = Val _; _ }; _ } -> return a + | Ptr { base; offset } -> let+ offset = select_i32 offset in - Expr.make (Ptr (base, Symbolic_value.const_i32 offset)) + Expr.ptr base (Symbolic_value.const_i32 offset) | _ -> let+ v = select_i32 a in Symbolic_value.const_i32 v diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml index bdd129e73..3ac62f85e 100644 --- a/src/symbolic/symbolic_memory.ml +++ b/src/symbolic/symbolic_memory.ml @@ -179,7 +179,7 @@ let get_limit_max _m = None (* TODO *) let check_within_bounds m a = match view a with | Val (Num (I32 _)) -> Ok (Value.Bool.const false, a) - | Ptr (base, offset) -> ( + | Ptr { base; offset } -> ( match Hashtbl.find m.chunks base with | exception Not_found -> Error Trap.Memory_leak_use_after_free | size -> diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index 97f420c59..791c7f51c 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -61,7 +61,7 @@ module M : let ptr v : int32 Choice.t = match view v with - | Ptr (b, _) -> Choice.return b + | Ptr { base; _ } -> Choice.return base | _ -> Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v; Choice.bind (abort ()) (fun () -> assert false) @@ -77,7 +77,7 @@ module M : Symbolic_memory.replace_size m base size ) tbl ) memories; - Expr.make (Ptr (base, Value.const_i32 0l)) ) ) + Expr.ptr base (Value.const_i32 0l) ) ) let free (p : Value.int32) : unit Choice.t = Choice.bind (ptr p) (fun base ->