wip

src/concolic/concolic.ml

@@ -2,6 +2,8 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
+module Symbolic_memory = Symbolic_memory_original
+
 module P = struct
   type thread = Concolic_choice.thread
 
@@ -209,8 +211,8 @@ module P = struct
       let orig_mem = Link_env.get_memory env id in
       let f (t : thread) : Memory.t =
         let sym_mem =
-          Symbolic_memory.get_memory (Link_env.id env) orig_mem
-            t.shared.memories id
+          Symbolic_memory_id.get_memory (Link_env.id env) orig_mem
+            t.shared.memories id Symbolic_memory.create
         in
         { concrete = orig_mem; symbolic = sym_mem }
       in

src/concolic/concolic_choice.ml

@@ -39,7 +39,7 @@ let pc_to_exprs pc = List.filter_map pc_elt_to_expr pc
 type pc = pc_elt list
 
 type shared_thread_info =
-  { memories : Symbolic_memory.collection
+  { memories : Symbolic_memory_original.t Symbolic_memory_id.collection
   ; tables : Symbolic_table.collection
   ; globals : Symbolic_global.collection
   }
@@ -147,7 +147,7 @@ let with_new_symbol ty f =
 
 let run preallocated_values (M v) : _ run_result =
   let shared =
-    { memories = Symbolic_memory.init ()
+    { memories = Symbolic_memory_id.init ()
     ; tables = Symbolic_table.init ()
     ; globals = Symbolic_global.init ()
     }

src/dune

@@ -29,6 +29,7 @@
   concolic_value
   concolic_wasm_ffi
   concrete
+  concrete_address_backend
   concrete_choice
   concrete_global
   concrete_memory
@@ -66,6 +67,10 @@
   symbolic_choice_without_memory
   symbolic_global
   symbolic_memory
+  symbolic_memory_id
+  symbolic_memory_intf
+  symbolic_memory_original
+  symbolic_memory_branching
   symbolic_table
   symbolic_value
   symbolic_wasm_ffi

src/intf/thread_intf.ml

@@ -3,11 +3,11 @@
 (* Written by the Owi programmers *)
 
 module type M = sig
-  type collection
+  type t
 
-  val init : unit -> collection
+  val create : int32 -> t
 
-  val clone : collection -> collection
+  val clone : t -> t
 end
 
 module type S = sig
@@ -21,15 +21,15 @@ module type S = sig
        int
     -> Smtml.Symbol.t list
     -> Symbolic_value.vbool list
-    -> Memory.collection
+    -> Memory.t Symbolic_memory_id.collection
     -> Symbolic_table.collection
     -> Symbolic_global.collection
     -> int32 list
     -> t
 
   val pc : t -> Symbolic_value.vbool list
 
-  val memories : t -> Memory.collection
+  val memories : t -> Memory.t Symbolic_memory_id.collection
 
   val tables : t -> Symbolic_table.collection
 
@@ -52,20 +52,10 @@ module type S = sig
   val incr_symbols : t -> t
 end
 
-module type S_with_memory =
-  S with type Memory.collection = Symbolic_memory.collection
-
-module type S_without_memory = S with type Memory.collection = bool
-
 module type Intf = sig
-  module type M = M
-
   module type S = S
 
-  module type S_with_memory = S_with_memory
-
-  module type S_without_memory = S_without_memory
+  module type M = M
 
-  module Make (Symbolic_memory : M) :
-    S with type Memory.collection = Symbolic_memory.collection
+  module Make (Symbolic_memory : M) : S with type Memory.t = Symbolic_memory.t
 end

src/symbolic/.symbolic_memory.mli

@@ -0,0 +1,96 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+type t
+
+type collection
+
+val init : unit -> collection
+
+val clone : collection -> collection
+
+val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
+
+val check_within_bounds :
+     t
+  -> Smtml.Expr.t
+  -> (Smtml.Expr.t * Symbolic_value.int32, Trap.t) result
+     Symbolic_choice_without_memory.t
+
+val replace_size : t -> Int32.t -> Smtml.Expr.t -> unit
+
+val free : t -> Int32.t -> unit
+
+val load_8_s :
+  t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+val load_8_u :
+  t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+val load_16_s :
+  t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+val load_16_u :
+  t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+val load_32 :
+  t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+val load_64 :
+  t -> Smtml.Expr.t -> Symbolic_value.int32 Symbolic_choice_without_memory.t
+
+val store_8 :
+     t
+  -> addr:Smtml.Expr.t
+  -> Smtml.Expr.t
+  -> unit Symbolic_choice_without_memory.t
+
+val store_16 :
+     t
+  -> addr:Smtml.Expr.t
+  -> Smtml.Expr.t
+  -> unit Symbolic_choice_without_memory.t
+
+val store_32 :
+     t
+  -> addr:Smtml.Expr.t
+  -> Smtml.Expr.t
+  -> unit Symbolic_choice_without_memory.t
+
+val store_64 :
+     t
+  -> addr:Smtml.Expr.t
+  -> Smtml.Expr.t
+  -> unit Symbolic_choice_without_memory.t
+
+val grow : t -> Smtml.Expr.t -> unit
+
+val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
+
+val blit :
+  t -> src:Smtml.Expr.t -> dst:Smtml.Expr.t -> len:Smtml.Expr.t -> Smtml.Expr.t
+
+val blit_string :
+     t
+  -> string
+  -> src:Smtml.Expr.t
+  -> dst:Smtml.Expr.t
+  -> len:Smtml.Expr.t
+  -> Smtml.Expr.t
+
+val size : t -> Smtml.Expr.t
+
+val size_in_pages : t -> Smtml.Expr.t
+
+val get_limit_max : t -> Smtml.Expr.t option
+
+module ITbl : sig
+  type 'a t
+
+  type key
+
+  val iter : (key -> 'a -> unit) -> 'a t -> unit
+end
+
+val iter : (t ITbl.t -> unit) -> collection -> unit

src/symbolic/concrete_address_backend.ml

@@ -0,0 +1,128 @@
+module Make (Choice : Choice_intf.Base with module V := Symbolic_value) :
+  Symbolic_memory_intf.M with type 'a m := 'a Choice.t = struct
+  open Choice
+
+  type address = Int32.t
+
+  type t =
+    { data : (address, Symbolic_value.int32) Hashtbl.t
+    ; parent : t option
+    ; chunks : (address, Symbolic_value.int32) Hashtbl.t
+    }
+
+  let make () =
+    { data = Hashtbl.create 128; parent = None; chunks = Hashtbl.create 16 }
+
+  let clone m =
+    { data = Hashtbl.create 16
+    ; parent = Some m
+    ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *)
+    }
+
+  let address v = select_i32 v
+
+  let address_i32 = Fun.id
+
+  let rec load_byte { parent; data; _ } a =
+    try Hashtbl.find data a
+    with Not_found -> (
+      match parent with
+      | None -> Smtml.Expr.value (Num (I8 0))
+      | Some parent -> load_byte parent a )
+
+  (* TODO: don't rebuild so many values it generates unecessary hc lookups *)
+  let merge_extracts (e1, h, m1) (e2, m2, l) =
+    let open Smtml.Expr in
+    let ty = ty e1 in
+    if m1 = m2 && equal e1 e2 then
+      if h - l = Smtml.Ty.size ty then e1 else make (Extract (e1, h, l))
+    else make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l))))
+
+  let concat ~msb ~lsb offset =
+    let open Smtml.Expr in
+    assert (offset > 0 && offset <= 8);
+    match (view msb, view lsb) with
+    | Val (Num (I8 i1)), Val (Num (I8 i2)) ->
+      Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2))
+    | Val (Num (I8 i1)), Val (Num (I32 i2)) ->
+      let offset = offset * 8 in
+      if offset < 32 then
+        Symbolic_value.const_i32
+          Int32.(logor (shl (of_int i1) (of_int offset)) i2)
+      else
+        let i1' = Int64.of_int i1 in
+        let i2' = Int64.of_int32 i2 in
+        Symbolic_value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2')
+    | Val (Num (I8 i1)), Val (Num (I64 i2)) ->
+      let offset = Int64.of_int (offset * 8) in
+      Symbolic_value.const_i64 Int64.(logor (shl (of_int i1) offset) i2)
+    | Extract (e1, h, m1), Extract (e2, m2, l) ->
+      merge_extracts (e1, h, m1) (e2, m2, l)
+    | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) ->
+      make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))
+    | _ -> make (Concat (msb, lsb))
+
+  let loadn m a n =
+    let rec loop addr size i acc =
+      if i = size then acc
+      else
+        let addr' = Int32.(add addr (of_int i)) in
+        let byte = load_byte m addr' in
+        loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc)
+    in
+    let v0 = load_byte m a in
+    loop a n 1 v0
+
+  let extract v pos =
+    let open Smtml.Expr in
+    match view v with
+    | Val (Num (I8 _)) -> v
+    | Val (Num (I32 i)) ->
+      let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in
+      value (Num (I8 i'))
+    | Val (Num (I64 i)) ->
+      let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in
+      value (Num (I8 i'))
+    | Cvtop
+        ( _
+        , (Zero_extend 24 | Sign_extend 24)
+        , ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym) ) ->
+      sym
+    | _ -> make (Extract (v, pos + 1, pos))
+
+  let storen m a v n =
+    for i = 0 to n - 1 do
+      let addr = Int32.add a (Int32.of_int i) in
+      let v = extract v i in
+      Hashtbl.replace m.data addr v
+    done
+
+  let must_be_within_bounds m a =
+    let open Smtml.Expr in
+    match view a with
+    | Val (Num (I32 a)) -> return (Ok a)
+    | Ptr { base; offset } -> (
+      match Hashtbl.find m.chunks base with
+      | exception Not_found -> return (Error Trap.Memory_leak_use_after_free)
+      | size ->
+        let base = Symbolic_value.const_i32 base in
+        let ptr = Symbolic_value.(I32.add base offset) in
+        let ub = Symbolic_value.(I32.ge ptr (I32.add base size)) in
+        let lb = Symbolic_value.I32.lt ptr base in
+        let* is_out_of_bounds = select (Symbolic_value.Bool.or_ lb ub) in
+        if is_out_of_bounds then return (Error Trap.Memory_heap_buffer_overflow)
+        else
+          let+ ptr = select_i32 ptr in
+          Ok ptr )
+    | _ ->
+      (* Log.err {|Unable to calculate address of: "%a"|} pp a *)
+      let+ ptr = select_i32 a in
+      Ok ptr
+
+  let free m base =
+    if not @@ Hashtbl.mem m.chunks base then
+      Fmt.failwith "Memory leak double free";
+    Hashtbl.remove m.chunks base
+
+  let realloc m base size = Hashtbl.replace m.chunks base size
+end