Fixes Ptr smtml change

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 -> *)

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

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 ->

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 ->